From: Enrico Tassi Date: Fri, 25 May 2007 08:17:37 +0000 (+0000) Subject: auto --> autobatch X-Git-Tag: 0.4.95@7852~437 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0e7999b2d7cb926affcf406f33e01e74bea62d7;p=helm.git auto --> autobatch --- diff --git a/matita/tests/TPTP/Veloci/BOO001-1.p.ma b/matita/tests/TPTP/Veloci/BOO001-1.p.ma index 4cc2223d1..38c012e5a 100644 --- a/matita/tests/TPTP/Veloci/BOO001-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO003-2.p.ma b/matita/tests/TPTP/Veloci/BOO003-2.p.ma index 93b11c287..cbbae8bea 100644 --- a/matita/tests/TPTP/Veloci/BOO003-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO003-4.p.ma b/matita/tests/TPTP/Veloci/BOO003-4.p.ma index 89dfcf314..b5fed12ac 100644 --- a/matita/tests/TPTP/Veloci/BOO003-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO004-2.p.ma b/matita/tests/TPTP/Veloci/BOO004-2.p.ma index 4ea34f1e0..cd5cb41d8 100644 --- a/matita/tests/TPTP/Veloci/BOO004-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO004-4.p.ma b/matita/tests/TPTP/Veloci/BOO004-4.p.ma index 9542f452a..c173d004c 100644 --- a/matita/tests/TPTP/Veloci/BOO004-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO005-2.p.ma b/matita/tests/TPTP/Veloci/BOO005-2.p.ma index c098b6cfb..e3e65f488 100644 --- a/matita/tests/TPTP/Veloci/BOO005-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO005-4.p.ma b/matita/tests/TPTP/Veloci/BOO005-4.p.ma index 04f83193c..655401b34 100644 --- a/matita/tests/TPTP/Veloci/BOO005-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO006-2.p.ma b/matita/tests/TPTP/Veloci/BOO006-2.p.ma index 0fd7e320c..69b96f774 100644 --- a/matita/tests/TPTP/Veloci/BOO006-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO006-4.p.ma b/matita/tests/TPTP/Veloci/BOO006-4.p.ma index 4a04acbd9..6b9db399f 100644 --- a/matita/tests/TPTP/Veloci/BOO006-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO009-2.p.ma b/matita/tests/TPTP/Veloci/BOO009-2.p.ma index 3328ed780..201ba75c3 100644 --- a/matita/tests/TPTP/Veloci/BOO009-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO009-4.p.ma b/matita/tests/TPTP/Veloci/BOO009-4.p.ma index fd724a6a3..1987e3b12 100644 --- a/matita/tests/TPTP/Veloci/BOO009-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO010-2.p.ma b/matita/tests/TPTP/Veloci/BOO010-2.p.ma index 8178f4043..f177f9c74 100644 --- a/matita/tests/TPTP/Veloci/BOO010-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO010-4.p.ma b/matita/tests/TPTP/Veloci/BOO010-4.p.ma index 764399c39..7b22061df 100644 --- a/matita/tests/TPTP/Veloci/BOO010-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO011-2.p.ma b/matita/tests/TPTP/Veloci/BOO011-2.p.ma index 94fafbca7..b0c35a767 100644 --- a/matita/tests/TPTP/Veloci/BOO011-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO011-4.p.ma b/matita/tests/TPTP/Veloci/BOO011-4.p.ma index 6451f3bd7..3353f8df4 100644 --- a/matita/tests/TPTP/Veloci/BOO011-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO012-2.p.ma b/matita/tests/TPTP/Veloci/BOO012-2.p.ma index 2823a4114..209840c60 100644 --- a/matita/tests/TPTP/Veloci/BOO012-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO012-4.p.ma b/matita/tests/TPTP/Veloci/BOO012-4.p.ma index bdd9c07e8..a3bfe1c4b 100644 --- a/matita/tests/TPTP/Veloci/BOO012-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO013-2.p.ma b/matita/tests/TPTP/Veloci/BOO013-2.p.ma index 202b96c7d..1b7800d75 100644 --- a/matita/tests/TPTP/Veloci/BOO013-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO013-4.p.ma b/matita/tests/TPTP/Veloci/BOO013-4.p.ma index 2eab59e4f..446b2b473 100644 --- a/matita/tests/TPTP/Veloci/BOO013-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO016-2.p.ma b/matita/tests/TPTP/Veloci/BOO016-2.p.ma index 91aec5ae7..a8d1ab9e7 100644 --- a/matita/tests/TPTP/Veloci/BOO016-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO017-2.p.ma b/matita/tests/TPTP/Veloci/BOO017-2.p.ma index ba23e0205..60ded0c1a 100644 --- a/matita/tests/TPTP/Veloci/BOO017-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO018-4.p.ma b/matita/tests/TPTP/Veloci/BOO018-4.p.ma index 6d6f2ab06..8e2774c34 100644 --- a/matita/tests/TPTP/Veloci/BOO018-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO034-1.p.ma b/matita/tests/TPTP/Veloci/BOO034-1.p.ma index a1626bf6d..e1f26e13d 100644 --- a/matita/tests/TPTP/Veloci/BOO034-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO069-1.p.ma b/matita/tests/TPTP/Veloci/BOO069-1.p.ma index 123624d1b..f76194c67 100644 --- a/matita/tests/TPTP/Veloci/BOO069-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO071-1.p.ma b/matita/tests/TPTP/Veloci/BOO071-1.p.ma index d76c4142c..806df9654 100644 --- a/matita/tests/TPTP/Veloci/BOO071-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/BOO075-1.p.ma b/matita/tests/TPTP/Veloci/BOO075-1.p.ma index 1f399f862..7f6d96d3c 100644 --- a/matita/tests/TPTP/Veloci/BOO075-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL004-3.p.ma b/matita/tests/TPTP/Veloci/COL004-3.p.ma index c2cf3ecbc..d88025c42 100644 --- a/matita/tests/TPTP/Veloci/COL004-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL007-1.p.ma b/matita/tests/TPTP/Veloci/COL007-1.p.ma index 6154d8a34..7018646d3 100644 --- a/matita/tests/TPTP/Veloci/COL007-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL008-1.p.ma b/matita/tests/TPTP/Veloci/COL008-1.p.ma index e8f9b3467..deee838a4 100644 --- a/matita/tests/TPTP/Veloci/COL008-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL010-1.p.ma b/matita/tests/TPTP/Veloci/COL010-1.p.ma index d8da7dbe8..61e95267a 100644 --- a/matita/tests/TPTP/Veloci/COL010-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL012-1.p.ma b/matita/tests/TPTP/Veloci/COL012-1.p.ma index 5b38f0dd8..5aba07935 100644 --- a/matita/tests/TPTP/Veloci/COL012-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL013-1.p.ma b/matita/tests/TPTP/Veloci/COL013-1.p.ma index 6ff4fddd1..ee3f5f7ba 100644 --- a/matita/tests/TPTP/Veloci/COL013-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL014-1.p.ma b/matita/tests/TPTP/Veloci/COL014-1.p.ma index 2e179255d..ef4e82edd 100644 --- a/matita/tests/TPTP/Veloci/COL014-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL015-1.p.ma b/matita/tests/TPTP/Veloci/COL015-1.p.ma index d2cc7be9f..2f4b47272 100644 --- a/matita/tests/TPTP/Veloci/COL015-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL016-1.p.ma b/matita/tests/TPTP/Veloci/COL016-1.p.ma index 5e84cf277..b655e805a 100644 --- a/matita/tests/TPTP/Veloci/COL016-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL017-1.p.ma b/matita/tests/TPTP/Veloci/COL017-1.p.ma index e6db2d319..eb063cf1e 100644 --- a/matita/tests/TPTP/Veloci/COL017-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL018-1.p.ma b/matita/tests/TPTP/Veloci/COL018-1.p.ma index 4aca85e92..87b023fdf 100644 --- a/matita/tests/TPTP/Veloci/COL018-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL021-1.p.ma b/matita/tests/TPTP/Veloci/COL021-1.p.ma index 144fac75b..612537946 100644 --- a/matita/tests/TPTP/Veloci/COL021-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL022-1.p.ma b/matita/tests/TPTP/Veloci/COL022-1.p.ma index b8b90725b..866d0abd7 100644 --- a/matita/tests/TPTP/Veloci/COL022-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL024-1.p.ma b/matita/tests/TPTP/Veloci/COL024-1.p.ma index 0ade23762..5476a13a1 100644 --- a/matita/tests/TPTP/Veloci/COL024-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL025-1.p.ma b/matita/tests/TPTP/Veloci/COL025-1.p.ma index 7a21954e5..d5c98aabf 100644 --- a/matita/tests/TPTP/Veloci/COL025-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL045-1.p.ma b/matita/tests/TPTP/Veloci/COL045-1.p.ma index 724503625..6ea3f3676 100644 --- a/matita/tests/TPTP/Veloci/COL045-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL048-1.p.ma b/matita/tests/TPTP/Veloci/COL048-1.p.ma index 728762834..bee9580b0 100644 --- a/matita/tests/TPTP/Veloci/COL048-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL050-1.p.ma b/matita/tests/TPTP/Veloci/COL050-1.p.ma index 662e3d7cd..716626e84 100644 --- a/matita/tests/TPTP/Veloci/COL050-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL058-2.p.ma b/matita/tests/TPTP/Veloci/COL058-2.p.ma index 86a05a99b..b0e94a980 100644 --- a/matita/tests/TPTP/Veloci/COL058-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL058-3.p.ma b/matita/tests/TPTP/Veloci/COL058-3.p.ma index f3e5b5d52..32802b0c5 100644 --- a/matita/tests/TPTP/Veloci/COL058-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL060-2.p.ma b/matita/tests/TPTP/Veloci/COL060-2.p.ma index 746e14da2..8ed2fdd81 100644 --- a/matita/tests/TPTP/Veloci/COL060-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL060-3.p.ma b/matita/tests/TPTP/Veloci/COL060-3.p.ma index 24ccd93b4..e33abe6e7 100644 --- a/matita/tests/TPTP/Veloci/COL060-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL061-2.p.ma b/matita/tests/TPTP/Veloci/COL061-2.p.ma index 41779cae6..14e0f74a0 100644 --- a/matita/tests/TPTP/Veloci/COL061-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL061-3.p.ma b/matita/tests/TPTP/Veloci/COL061-3.p.ma index a59f55f4b..ca9a9653d 100644 --- a/matita/tests/TPTP/Veloci/COL061-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL062-2.p.ma b/matita/tests/TPTP/Veloci/COL062-2.p.ma index b366a3f9f..839f6ae93 100644 --- a/matita/tests/TPTP/Veloci/COL062-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL062-3.p.ma b/matita/tests/TPTP/Veloci/COL062-3.p.ma index 3734fb971..5b8ad716e 100644 --- a/matita/tests/TPTP/Veloci/COL062-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL063-2.p.ma b/matita/tests/TPTP/Veloci/COL063-2.p.ma index 1857b0fba..31a6ae8ec 100644 --- a/matita/tests/TPTP/Veloci/COL063-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL063-3.p.ma b/matita/tests/TPTP/Veloci/COL063-3.p.ma index fddb0328a..1c5133b0e 100644 --- a/matita/tests/TPTP/Veloci/COL063-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL063-4.p.ma b/matita/tests/TPTP/Veloci/COL063-4.p.ma index 6f4ebb664..b341b737b 100644 --- a/matita/tests/TPTP/Veloci/COL063-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL063-5.p.ma b/matita/tests/TPTP/Veloci/COL063-5.p.ma index 636fa6b6d..22976148e 100644 --- a/matita/tests/TPTP/Veloci/COL063-5.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL063-6.p.ma b/matita/tests/TPTP/Veloci/COL063-6.p.ma index e60af56ce..b7c423748 100644 --- a/matita/tests/TPTP/Veloci/COL063-6.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL064-2.p.ma b/matita/tests/TPTP/Veloci/COL064-2.p.ma index a179cceba..5b45bc7ea 100644 --- a/matita/tests/TPTP/Veloci/COL064-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL064-3.p.ma b/matita/tests/TPTP/Veloci/COL064-3.p.ma index 2d2bbc7c5..88b85eb9b 100644 --- a/matita/tests/TPTP/Veloci/COL064-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL064-4.p.ma b/matita/tests/TPTP/Veloci/COL064-4.p.ma index 9c6113ada..c1690d065 100644 --- a/matita/tests/TPTP/Veloci/COL064-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL064-5.p.ma b/matita/tests/TPTP/Veloci/COL064-5.p.ma index dd0f1ffbe..989b3c1bf 100644 --- a/matita/tests/TPTP/Veloci/COL064-5.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL064-6.p.ma b/matita/tests/TPTP/Veloci/COL064-6.p.ma index dfdc9b00d..cb5635f98 100644 --- a/matita/tests/TPTP/Veloci/COL064-6.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL064-7.p.ma b/matita/tests/TPTP/Veloci/COL064-7.p.ma index f2cb5118f..d7a0a9cab 100644 --- a/matita/tests/TPTP/Veloci/COL064-7.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL064-8.p.ma b/matita/tests/TPTP/Veloci/COL064-8.p.ma index cc05447be..89111c679 100644 --- a/matita/tests/TPTP/Veloci/COL064-8.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL064-9.p.ma b/matita/tests/TPTP/Veloci/COL064-9.p.ma index 362338108..8e6ad6cdb 100644 --- a/matita/tests/TPTP/Veloci/COL064-9.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL083-1.p.ma b/matita/tests/TPTP/Veloci/COL083-1.p.ma index 02fbbcabb..870b7d862 100644 --- a/matita/tests/TPTP/Veloci/COL083-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL084-1.p.ma b/matita/tests/TPTP/Veloci/COL084-1.p.ma index a1c8dd0ab..f345021bf 100644 --- a/matita/tests/TPTP/Veloci/COL084-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL085-1.p.ma b/matita/tests/TPTP/Veloci/COL085-1.p.ma index fe71489cf..ff1981363 100644 --- a/matita/tests/TPTP/Veloci/COL085-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/COL086-1.p.ma b/matita/tests/TPTP/Veloci/COL086-1.p.ma index 0f7c24aa0..030c2cd33 100644 --- a/matita/tests/TPTP/Veloci/COL086-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP001-2.p.ma b/matita/tests/TPTP/Veloci/GRP001-2.p.ma index fcb3b6afd..c695b7f80 100644 --- a/matita/tests/TPTP/Veloci/GRP001-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP001-4.p.ma b/matita/tests/TPTP/Veloci/GRP001-4.p.ma index 1011802d4..ea943fdd8 100644 --- a/matita/tests/TPTP/Veloci/GRP001-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP010-4.p.ma b/matita/tests/TPTP/Veloci/GRP010-4.p.ma index 83be67ecf..ce5111529 100644 --- a/matita/tests/TPTP/Veloci/GRP010-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP011-4.p.ma b/matita/tests/TPTP/Veloci/GRP011-4.p.ma index 3bf8fe21a..d11f4a5f4 100644 --- a/matita/tests/TPTP/Veloci/GRP011-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP012-4.p.ma b/matita/tests/TPTP/Veloci/GRP012-4.p.ma index f97360370..4d7966963 100644 --- a/matita/tests/TPTP/Veloci/GRP012-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP022-2.p.ma b/matita/tests/TPTP/Veloci/GRP022-2.p.ma index 4e0da1e47..034f854c3 100644 --- a/matita/tests/TPTP/Veloci/GRP022-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP023-2.p.ma b/matita/tests/TPTP/Veloci/GRP023-2.p.ma index afeda0d1f..f5cb37252 100644 --- a/matita/tests/TPTP/Veloci/GRP023-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP115-1.p.ma b/matita/tests/TPTP/Veloci/GRP115-1.p.ma index 773068e1f..dafda9a6e 100644 --- a/matita/tests/TPTP/Veloci/GRP115-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP116-1.p.ma b/matita/tests/TPTP/Veloci/GRP116-1.p.ma index e6bf5c0b2..d7895138b 100644 --- a/matita/tests/TPTP/Veloci/GRP116-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP117-1.p.ma b/matita/tests/TPTP/Veloci/GRP117-1.p.ma index e33eac2ac..2d04443b6 100644 --- a/matita/tests/TPTP/Veloci/GRP117-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP118-1.p.ma b/matita/tests/TPTP/Veloci/GRP118-1.p.ma index 562cd1811..d348a57db 100644 --- a/matita/tests/TPTP/Veloci/GRP118-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP136-1.p.ma b/matita/tests/TPTP/Veloci/GRP136-1.p.ma index 7736d1567..b3380a855 100644 --- a/matita/tests/TPTP/Veloci/GRP136-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP137-1.p.ma b/matita/tests/TPTP/Veloci/GRP137-1.p.ma index f570845cd..34885590c 100644 --- a/matita/tests/TPTP/Veloci/GRP137-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP139-1.p.ma b/matita/tests/TPTP/Veloci/GRP139-1.p.ma index 6847c52b6..1e3644eae 100644 --- a/matita/tests/TPTP/Veloci/GRP139-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP141-1.p.ma b/matita/tests/TPTP/Veloci/GRP141-1.p.ma index 40442e00a..6b7b50871 100644 --- a/matita/tests/TPTP/Veloci/GRP141-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP142-1.p.ma b/matita/tests/TPTP/Veloci/GRP142-1.p.ma index 0727c7051..ac52f8966 100644 --- a/matita/tests/TPTP/Veloci/GRP142-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP143-1.p.ma b/matita/tests/TPTP/Veloci/GRP143-1.p.ma index 887c1ba02..cefbb9734 100644 --- a/matita/tests/TPTP/Veloci/GRP143-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP144-1.p.ma b/matita/tests/TPTP/Veloci/GRP144-1.p.ma index 3d19c2c02..920463e12 100644 --- a/matita/tests/TPTP/Veloci/GRP144-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP145-1.p.ma b/matita/tests/TPTP/Veloci/GRP145-1.p.ma index bbce5c045..63b6c5087 100644 --- a/matita/tests/TPTP/Veloci/GRP145-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP146-1.p.ma b/matita/tests/TPTP/Veloci/GRP146-1.p.ma index ce184d7d1..2c39e935d 100644 --- a/matita/tests/TPTP/Veloci/GRP146-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP149-1.p.ma b/matita/tests/TPTP/Veloci/GRP149-1.p.ma index bdbd3df36..9030600cb 100644 --- a/matita/tests/TPTP/Veloci/GRP149-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP150-1.p.ma b/matita/tests/TPTP/Veloci/GRP150-1.p.ma index bb79b6b40..ceae01410 100644 --- a/matita/tests/TPTP/Veloci/GRP150-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP151-1.p.ma b/matita/tests/TPTP/Veloci/GRP151-1.p.ma index d1f8a8f4e..454c61546 100644 --- a/matita/tests/TPTP/Veloci/GRP151-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP152-1.p.ma b/matita/tests/TPTP/Veloci/GRP152-1.p.ma index a657802e9..941fc726c 100644 --- a/matita/tests/TPTP/Veloci/GRP152-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP153-1.p.ma b/matita/tests/TPTP/Veloci/GRP153-1.p.ma index 5fb6b6928..c677c140c 100644 --- a/matita/tests/TPTP/Veloci/GRP153-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP154-1.p.ma b/matita/tests/TPTP/Veloci/GRP154-1.p.ma index 0212ea903..04245f9de 100644 --- a/matita/tests/TPTP/Veloci/GRP154-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP155-1.p.ma b/matita/tests/TPTP/Veloci/GRP155-1.p.ma index 7531e2af3..b7149e55f 100644 --- a/matita/tests/TPTP/Veloci/GRP155-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP156-1.p.ma b/matita/tests/TPTP/Veloci/GRP156-1.p.ma index 0f55687c1..db0a9b38f 100644 --- a/matita/tests/TPTP/Veloci/GRP156-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP157-1.p.ma b/matita/tests/TPTP/Veloci/GRP157-1.p.ma index 98bb06522..10948cac5 100644 --- a/matita/tests/TPTP/Veloci/GRP157-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP158-1.p.ma b/matita/tests/TPTP/Veloci/GRP158-1.p.ma index f725b2f7b..269be4042 100644 --- a/matita/tests/TPTP/Veloci/GRP158-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP159-1.p.ma b/matita/tests/TPTP/Veloci/GRP159-1.p.ma index 90c11d85a..1a9471a66 100644 --- a/matita/tests/TPTP/Veloci/GRP159-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP160-1.p.ma b/matita/tests/TPTP/Veloci/GRP160-1.p.ma index 383b0e2d1..0aa320f7d 100644 --- a/matita/tests/TPTP/Veloci/GRP160-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP161-1.p.ma b/matita/tests/TPTP/Veloci/GRP161-1.p.ma index 29a70eadc..473d47bc4 100644 --- a/matita/tests/TPTP/Veloci/GRP161-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP162-1.p.ma b/matita/tests/TPTP/Veloci/GRP162-1.p.ma index 03ee7c53f..c1af39429 100644 --- a/matita/tests/TPTP/Veloci/GRP162-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP163-1.p.ma b/matita/tests/TPTP/Veloci/GRP163-1.p.ma index e6fc69f78..964662f6c 100644 --- a/matita/tests/TPTP/Veloci/GRP163-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP168-1.p.ma b/matita/tests/TPTP/Veloci/GRP168-1.p.ma index 18243968e..162fcd775 100644 --- a/matita/tests/TPTP/Veloci/GRP168-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP168-2.p.ma b/matita/tests/TPTP/Veloci/GRP168-2.p.ma index bcf26d5d9..ff7f06967 100644 --- a/matita/tests/TPTP/Veloci/GRP168-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP173-1.p.ma b/matita/tests/TPTP/Veloci/GRP173-1.p.ma index 849057bc5..34791231e 100644 --- a/matita/tests/TPTP/Veloci/GRP173-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP174-1.p.ma b/matita/tests/TPTP/Veloci/GRP174-1.p.ma index 076784ef8..77177b3f5 100644 --- a/matita/tests/TPTP/Veloci/GRP174-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP176-1.p.ma b/matita/tests/TPTP/Veloci/GRP176-1.p.ma index b67193505..485cd7c0e 100644 --- a/matita/tests/TPTP/Veloci/GRP176-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP176-2.p.ma b/matita/tests/TPTP/Veloci/GRP176-2.p.ma index 33d15dcc3..e5dbe4ab7 100644 --- a/matita/tests/TPTP/Veloci/GRP176-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP182-1.p.ma b/matita/tests/TPTP/Veloci/GRP182-1.p.ma index 3b13987b5..25f4ec89d 100644 --- a/matita/tests/TPTP/Veloci/GRP182-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP182-2.p.ma b/matita/tests/TPTP/Veloci/GRP182-2.p.ma index 59f725c19..99d2f2272 100644 --- a/matita/tests/TPTP/Veloci/GRP182-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP182-3.p.ma b/matita/tests/TPTP/Veloci/GRP182-3.p.ma index 4c890fbd1..ad3388fcf 100644 --- a/matita/tests/TPTP/Veloci/GRP182-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP182-4.p.ma b/matita/tests/TPTP/Veloci/GRP182-4.p.ma index 1942f7064..c5f686a70 100644 --- a/matita/tests/TPTP/Veloci/GRP182-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP186-3.p.ma b/matita/tests/TPTP/Veloci/GRP186-3.p.ma index a358b5fd3..d5ba153b9 100644 --- a/matita/tests/TPTP/Veloci/GRP186-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP186-4.p.ma b/matita/tests/TPTP/Veloci/GRP186-4.p.ma index aac5c99e7..eb035cbbb 100644 --- a/matita/tests/TPTP/Veloci/GRP186-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP188-1.p.ma b/matita/tests/TPTP/Veloci/GRP188-1.p.ma index a4142e5c9..2ad492bcf 100644 --- a/matita/tests/TPTP/Veloci/GRP188-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP188-2.p.ma b/matita/tests/TPTP/Veloci/GRP188-2.p.ma index 043fc5af7..9008f3ef0 100644 --- a/matita/tests/TPTP/Veloci/GRP188-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP189-1.p.ma b/matita/tests/TPTP/Veloci/GRP189-1.p.ma index 47d76e5e2..d2fff5b3d 100644 --- a/matita/tests/TPTP/Veloci/GRP189-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP189-2.p.ma b/matita/tests/TPTP/Veloci/GRP189-2.p.ma index 7d8396675..eedb47810 100644 --- a/matita/tests/TPTP/Veloci/GRP189-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP192-1.p.ma b/matita/tests/TPTP/Veloci/GRP192-1.p.ma index cbfcff30c..8463afd62 100644 --- a/matita/tests/TPTP/Veloci/GRP192-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP206-1.p.ma b/matita/tests/TPTP/Veloci/GRP206-1.p.ma index 62ad0624c..bec8aa7f7 100644 --- a/matita/tests/TPTP/Veloci/GRP206-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP454-1.p.ma b/matita/tests/TPTP/Veloci/GRP454-1.p.ma index 9281a270a..a3f949d3e 100644 --- a/matita/tests/TPTP/Veloci/GRP454-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP455-1.p.ma b/matita/tests/TPTP/Veloci/GRP455-1.p.ma index ef2028982..c70c4f672 100644 --- a/matita/tests/TPTP/Veloci/GRP455-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP456-1.p.ma b/matita/tests/TPTP/Veloci/GRP456-1.p.ma index 1804cdb78..c5b9d8c5d 100644 --- a/matita/tests/TPTP/Veloci/GRP456-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP457-1.p.ma b/matita/tests/TPTP/Veloci/GRP457-1.p.ma index fcba4e4e7..3358805bc 100644 --- a/matita/tests/TPTP/Veloci/GRP457-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP458-1.p.ma b/matita/tests/TPTP/Veloci/GRP458-1.p.ma index 3d782b025..e297b3b08 100644 --- a/matita/tests/TPTP/Veloci/GRP458-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP459-1.p.ma b/matita/tests/TPTP/Veloci/GRP459-1.p.ma index 3ade69780..c3302ae0c 100644 --- a/matita/tests/TPTP/Veloci/GRP459-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP460-1.p.ma b/matita/tests/TPTP/Veloci/GRP460-1.p.ma index 6413b5743..7dcd0f698 100644 --- a/matita/tests/TPTP/Veloci/GRP460-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP463-1.p.ma b/matita/tests/TPTP/Veloci/GRP463-1.p.ma index 6bf794240..be1180422 100644 --- a/matita/tests/TPTP/Veloci/GRP463-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP467-1.p.ma b/matita/tests/TPTP/Veloci/GRP467-1.p.ma index 2ebeb9f5d..f7723d3c0 100644 --- a/matita/tests/TPTP/Veloci/GRP467-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP481-1.p.ma b/matita/tests/TPTP/Veloci/GRP481-1.p.ma index c4eaf5861..e5f0a50ed 100644 --- a/matita/tests/TPTP/Veloci/GRP481-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP484-1.p.ma b/matita/tests/TPTP/Veloci/GRP484-1.p.ma index b673ea1fe..746cf9541 100644 --- a/matita/tests/TPTP/Veloci/GRP484-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP485-1.p.ma b/matita/tests/TPTP/Veloci/GRP485-1.p.ma index 21831160b..63fe7d2a1 100644 --- a/matita/tests/TPTP/Veloci/GRP485-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP486-1.p.ma b/matita/tests/TPTP/Veloci/GRP486-1.p.ma index 264794f50..b8ecfd815 100644 --- a/matita/tests/TPTP/Veloci/GRP486-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP487-1.p.ma b/matita/tests/TPTP/Veloci/GRP487-1.p.ma index 51a728493..b679645fe 100644 --- a/matita/tests/TPTP/Veloci/GRP487-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP488-1.p.ma b/matita/tests/TPTP/Veloci/GRP488-1.p.ma index 0026f5c89..c6b63cbcf 100644 --- a/matita/tests/TPTP/Veloci/GRP488-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP490-1.p.ma b/matita/tests/TPTP/Veloci/GRP490-1.p.ma index fe07b798d..326e72502 100644 --- a/matita/tests/TPTP/Veloci/GRP490-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP491-1.p.ma b/matita/tests/TPTP/Veloci/GRP491-1.p.ma index 600af87e1..39482784f 100644 --- a/matita/tests/TPTP/Veloci/GRP491-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP492-1.p.ma b/matita/tests/TPTP/Veloci/GRP492-1.p.ma index 921714afd..3af993fcf 100644 --- a/matita/tests/TPTP/Veloci/GRP492-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP493-1.p.ma b/matita/tests/TPTP/Veloci/GRP493-1.p.ma index 8963ddaf8..059f6e300 100644 --- a/matita/tests/TPTP/Veloci/GRP493-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP494-1.p.ma b/matita/tests/TPTP/Veloci/GRP494-1.p.ma index 0e280132b..888ad8576 100644 --- a/matita/tests/TPTP/Veloci/GRP494-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP495-1.p.ma b/matita/tests/TPTP/Veloci/GRP495-1.p.ma index af079e663..8c6d03b3d 100644 --- a/matita/tests/TPTP/Veloci/GRP495-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP496-1.p.ma b/matita/tests/TPTP/Veloci/GRP496-1.p.ma index d655496c5..f96492e13 100644 --- a/matita/tests/TPTP/Veloci/GRP496-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP497-1.p.ma b/matita/tests/TPTP/Veloci/GRP497-1.p.ma index a7d1d5a8e..79e82ae64 100644 --- a/matita/tests/TPTP/Veloci/GRP497-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP498-1.p.ma b/matita/tests/TPTP/Veloci/GRP498-1.p.ma index e26c08db4..d2cac96d0 100644 --- a/matita/tests/TPTP/Veloci/GRP498-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP509-1.p.ma b/matita/tests/TPTP/Veloci/GRP509-1.p.ma index 0458df1fa..dfbaf1362 100644 --- a/matita/tests/TPTP/Veloci/GRP509-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP510-1.p.ma b/matita/tests/TPTP/Veloci/GRP510-1.p.ma index 146e6a814..7806668c0 100644 --- a/matita/tests/TPTP/Veloci/GRP510-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP511-1.p.ma b/matita/tests/TPTP/Veloci/GRP511-1.p.ma index 466126222..34d3bab74 100644 --- a/matita/tests/TPTP/Veloci/GRP511-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP512-1.p.ma b/matita/tests/TPTP/Veloci/GRP512-1.p.ma index e78bed00f..790814570 100644 --- a/matita/tests/TPTP/Veloci/GRP512-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP513-1.p.ma b/matita/tests/TPTP/Veloci/GRP513-1.p.ma index fdf42d748..022817297 100644 --- a/matita/tests/TPTP/Veloci/GRP513-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP514-1.p.ma b/matita/tests/TPTP/Veloci/GRP514-1.p.ma index 74dc8a63a..44411f118 100644 --- a/matita/tests/TPTP/Veloci/GRP514-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP515-1.p.ma b/matita/tests/TPTP/Veloci/GRP515-1.p.ma index 83eb4b753..2ad540b74 100644 --- a/matita/tests/TPTP/Veloci/GRP515-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP516-1.p.ma b/matita/tests/TPTP/Veloci/GRP516-1.p.ma index dde992a18..59a8da6ac 100644 --- a/matita/tests/TPTP/Veloci/GRP516-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP517-1.p.ma b/matita/tests/TPTP/Veloci/GRP517-1.p.ma index ee9bff2fc..e268d2534 100644 --- a/matita/tests/TPTP/Veloci/GRP517-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP518-1.p.ma b/matita/tests/TPTP/Veloci/GRP518-1.p.ma index 6ff2950a6..89a742ca1 100644 --- a/matita/tests/TPTP/Veloci/GRP518-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP520-1.p.ma b/matita/tests/TPTP/Veloci/GRP520-1.p.ma index 33f0bd79a..879b8f0a9 100644 --- a/matita/tests/TPTP/Veloci/GRP520-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP541-1.p.ma b/matita/tests/TPTP/Veloci/GRP541-1.p.ma index ab4a50104..446167f51 100644 --- a/matita/tests/TPTP/Veloci/GRP541-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP542-1.p.ma b/matita/tests/TPTP/Veloci/GRP542-1.p.ma index 37900e2ec..6e084eef4 100644 --- a/matita/tests/TPTP/Veloci/GRP542-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP543-1.p.ma b/matita/tests/TPTP/Veloci/GRP543-1.p.ma index efe72032b..2e80e0158 100644 --- a/matita/tests/TPTP/Veloci/GRP543-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP544-1.p.ma b/matita/tests/TPTP/Veloci/GRP544-1.p.ma index 66b15a5cf..3a5257ed0 100644 --- a/matita/tests/TPTP/Veloci/GRP544-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP545-1.p.ma b/matita/tests/TPTP/Veloci/GRP545-1.p.ma index 1e66b6585..e4caec04b 100644 --- a/matita/tests/TPTP/Veloci/GRP545-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP546-1.p.ma b/matita/tests/TPTP/Veloci/GRP546-1.p.ma index bc5433839..ba46f7f71 100644 --- a/matita/tests/TPTP/Veloci/GRP546-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP547-1.p.ma b/matita/tests/TPTP/Veloci/GRP547-1.p.ma index 5256be724..981df2d12 100644 --- a/matita/tests/TPTP/Veloci/GRP547-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP548-1.p.ma b/matita/tests/TPTP/Veloci/GRP548-1.p.ma index 91748c17f..8750ac7e8 100644 --- a/matita/tests/TPTP/Veloci/GRP548-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP549-1.p.ma b/matita/tests/TPTP/Veloci/GRP549-1.p.ma index eb94e08e2..9e5165b72 100644 --- a/matita/tests/TPTP/Veloci/GRP549-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP550-1.p.ma b/matita/tests/TPTP/Veloci/GRP550-1.p.ma index 69d89ee91..ceb1fcb92 100644 --- a/matita/tests/TPTP/Veloci/GRP550-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP551-1.p.ma b/matita/tests/TPTP/Veloci/GRP551-1.p.ma index 77abdbeea..69b83f64d 100644 --- a/matita/tests/TPTP/Veloci/GRP551-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP552-1.p.ma b/matita/tests/TPTP/Veloci/GRP552-1.p.ma index f04d0b10c..72d8dbb1a 100644 --- a/matita/tests/TPTP/Veloci/GRP552-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP556-1.p.ma b/matita/tests/TPTP/Veloci/GRP556-1.p.ma index f9dbfb85e..7ff2cf4fc 100644 --- a/matita/tests/TPTP/Veloci/GRP556-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP558-1.p.ma b/matita/tests/TPTP/Veloci/GRP558-1.p.ma index 09e45674e..d3ffe8859 100644 --- a/matita/tests/TPTP/Veloci/GRP558-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP560-1.p.ma b/matita/tests/TPTP/Veloci/GRP560-1.p.ma index e411b5724..f145a3af9 100644 --- a/matita/tests/TPTP/Veloci/GRP560-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP561-1.p.ma b/matita/tests/TPTP/Veloci/GRP561-1.p.ma index 396c9dd37..d6d1ef6ed 100644 --- a/matita/tests/TPTP/Veloci/GRP561-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP562-1.p.ma b/matita/tests/TPTP/Veloci/GRP562-1.p.ma index 0a2a60ff2..118adfa7a 100644 --- a/matita/tests/TPTP/Veloci/GRP562-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP564-1.p.ma b/matita/tests/TPTP/Veloci/GRP564-1.p.ma index df8fe3ff8..c46fb73d6 100644 --- a/matita/tests/TPTP/Veloci/GRP564-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP565-1.p.ma b/matita/tests/TPTP/Veloci/GRP565-1.p.ma index 5a76d9981..e9151448c 100644 --- a/matita/tests/TPTP/Veloci/GRP565-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP566-1.p.ma b/matita/tests/TPTP/Veloci/GRP566-1.p.ma index b647dce22..23b805f00 100644 --- a/matita/tests/TPTP/Veloci/GRP566-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP567-1.p.ma b/matita/tests/TPTP/Veloci/GRP567-1.p.ma index cf0a795d9..e77e2b762 100644 --- a/matita/tests/TPTP/Veloci/GRP567-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP568-1.p.ma b/matita/tests/TPTP/Veloci/GRP568-1.p.ma index 16cd566aa..07adcfd9b 100644 --- a/matita/tests/TPTP/Veloci/GRP568-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP569-1.p.ma b/matita/tests/TPTP/Veloci/GRP569-1.p.ma index 118437264..260522c05 100644 --- a/matita/tests/TPTP/Veloci/GRP569-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP570-1.p.ma b/matita/tests/TPTP/Veloci/GRP570-1.p.ma index 9720c564a..d74cd154f 100644 --- a/matita/tests/TPTP/Veloci/GRP570-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP572-1.p.ma b/matita/tests/TPTP/Veloci/GRP572-1.p.ma index f740a647f..270768037 100644 --- a/matita/tests/TPTP/Veloci/GRP572-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP573-1.p.ma b/matita/tests/TPTP/Veloci/GRP573-1.p.ma index 760a12564..1ae737d5b 100644 --- a/matita/tests/TPTP/Veloci/GRP573-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP574-1.p.ma b/matita/tests/TPTP/Veloci/GRP574-1.p.ma index 1f6da909a..a3d3395f5 100644 --- a/matita/tests/TPTP/Veloci/GRP574-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP576-1.p.ma b/matita/tests/TPTP/Veloci/GRP576-1.p.ma index 0f9ec0dbb..d192c0455 100644 --- a/matita/tests/TPTP/Veloci/GRP576-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP577-1.p.ma b/matita/tests/TPTP/Veloci/GRP577-1.p.ma index 418921649..e0836fded 100644 --- a/matita/tests/TPTP/Veloci/GRP577-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP578-1.p.ma b/matita/tests/TPTP/Veloci/GRP578-1.p.ma index e44ea55db..ef7d1793f 100644 --- a/matita/tests/TPTP/Veloci/GRP578-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP580-1.p.ma b/matita/tests/TPTP/Veloci/GRP580-1.p.ma index c37de12c2..aee50acd9 100644 --- a/matita/tests/TPTP/Veloci/GRP580-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP581-1.p.ma b/matita/tests/TPTP/Veloci/GRP581-1.p.ma index ccaa5e80e..76b98c5a2 100644 --- a/matita/tests/TPTP/Veloci/GRP581-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP582-1.p.ma b/matita/tests/TPTP/Veloci/GRP582-1.p.ma index 74691ad6d..2c1a81a7d 100644 --- a/matita/tests/TPTP/Veloci/GRP582-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP583-1.p.ma b/matita/tests/TPTP/Veloci/GRP583-1.p.ma index a82d60e88..eb1c927ec 100644 --- a/matita/tests/TPTP/Veloci/GRP583-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP584-1.p.ma b/matita/tests/TPTP/Veloci/GRP584-1.p.ma index e743542a3..b66e93f43 100644 --- a/matita/tests/TPTP/Veloci/GRP584-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP586-1.p.ma b/matita/tests/TPTP/Veloci/GRP586-1.p.ma index 5b2a189ec..9c4c69ed0 100644 --- a/matita/tests/TPTP/Veloci/GRP586-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP588-1.p.ma b/matita/tests/TPTP/Veloci/GRP588-1.p.ma index 66ef7c555..1c32572b0 100644 --- a/matita/tests/TPTP/Veloci/GRP588-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP590-1.p.ma b/matita/tests/TPTP/Veloci/GRP590-1.p.ma index c89d13252..3a8c3f132 100644 --- a/matita/tests/TPTP/Veloci/GRP590-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP592-1.p.ma b/matita/tests/TPTP/Veloci/GRP592-1.p.ma index 0e9eac474..c2c748817 100644 --- a/matita/tests/TPTP/Veloci/GRP592-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP595-1.p.ma b/matita/tests/TPTP/Veloci/GRP595-1.p.ma index 354515802..d17416172 100644 --- a/matita/tests/TPTP/Veloci/GRP595-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP596-1.p.ma b/matita/tests/TPTP/Veloci/GRP596-1.p.ma index 9def73c5f..45b171485 100644 --- a/matita/tests/TPTP/Veloci/GRP596-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP597-1.p.ma b/matita/tests/TPTP/Veloci/GRP597-1.p.ma index dd33c8ed7..3076cda7d 100644 --- a/matita/tests/TPTP/Veloci/GRP597-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP598-1.p.ma b/matita/tests/TPTP/Veloci/GRP598-1.p.ma index 06dfd2c5e..dfd966562 100644 --- a/matita/tests/TPTP/Veloci/GRP598-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP599-1.p.ma b/matita/tests/TPTP/Veloci/GRP599-1.p.ma index 1305cf6ce..f703d7b6b 100644 --- a/matita/tests/TPTP/Veloci/GRP599-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP600-1.p.ma b/matita/tests/TPTP/Veloci/GRP600-1.p.ma index 965637bc7..d8180ca64 100644 --- a/matita/tests/TPTP/Veloci/GRP600-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP602-1.p.ma b/matita/tests/TPTP/Veloci/GRP602-1.p.ma index 19b676eca..d2d0d3305 100644 --- a/matita/tests/TPTP/Veloci/GRP602-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP603-1.p.ma b/matita/tests/TPTP/Veloci/GRP603-1.p.ma index 3c25c6ffe..6ee5d33c5 100644 --- a/matita/tests/TPTP/Veloci/GRP603-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP604-1.p.ma b/matita/tests/TPTP/Veloci/GRP604-1.p.ma index 5b583615e..4e083dea9 100644 --- a/matita/tests/TPTP/Veloci/GRP604-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP605-1.p.ma b/matita/tests/TPTP/Veloci/GRP605-1.p.ma index e637e7d4a..0145a313e 100644 --- a/matita/tests/TPTP/Veloci/GRP605-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP606-1.p.ma b/matita/tests/TPTP/Veloci/GRP606-1.p.ma index 6f271dd69..4f4e2bea1 100644 --- a/matita/tests/TPTP/Veloci/GRP606-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP608-1.p.ma b/matita/tests/TPTP/Veloci/GRP608-1.p.ma index 77eef1f73..811ae06bc 100644 --- a/matita/tests/TPTP/Veloci/GRP608-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP612-1.p.ma b/matita/tests/TPTP/Veloci/GRP612-1.p.ma index c2656bf79..936eedbaa 100644 --- a/matita/tests/TPTP/Veloci/GRP612-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP613-1.p.ma b/matita/tests/TPTP/Veloci/GRP613-1.p.ma index 6bf34a806..5f5960ed6 100644 --- a/matita/tests/TPTP/Veloci/GRP613-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP614-1.p.ma b/matita/tests/TPTP/Veloci/GRP614-1.p.ma index 15eeca809..389785f55 100644 --- a/matita/tests/TPTP/Veloci/GRP614-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP615-1.p.ma b/matita/tests/TPTP/Veloci/GRP615-1.p.ma index ee30724b2..2f656b223 100644 --- a/matita/tests/TPTP/Veloci/GRP615-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/GRP616-1.p.ma b/matita/tests/TPTP/Veloci/GRP616-1.p.ma index 413d5d0d0..619a0f5bb 100644 --- a/matita/tests/TPTP/Veloci/GRP616-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LAT008-1.p.ma b/matita/tests/TPTP/Veloci/LAT008-1.p.ma index c9075f2e3..789549d1c 100644 --- a/matita/tests/TPTP/Veloci/LAT008-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LAT033-1.p.ma b/matita/tests/TPTP/Veloci/LAT033-1.p.ma index ba2e724eb..b5548d960 100644 --- a/matita/tests/TPTP/Veloci/LAT033-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LAT034-1.p.ma b/matita/tests/TPTP/Veloci/LAT034-1.p.ma index 548df9d84..801451c43 100644 --- a/matita/tests/TPTP/Veloci/LAT034-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LAT039-1.p.ma b/matita/tests/TPTP/Veloci/LAT039-1.p.ma index 570d23724..61d6cef04 100644 --- a/matita/tests/TPTP/Veloci/LAT039-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LAT039-2.p.ma b/matita/tests/TPTP/Veloci/LAT039-2.p.ma index 05e4b3cfd..c7af583bd 100644 --- a/matita/tests/TPTP/Veloci/LAT039-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/LAT040-1.p.ma b/matita/tests/TPTP/Veloci/LAT040-1.p.ma index ea3be43e0..9982a8eab 100644 --- a/matita/tests/TPTP/Veloci/LAT040-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LAT045-1.p.ma b/matita/tests/TPTP/Veloci/LAT045-1.p.ma index e2a7df884..f998f72e9 100644 --- a/matita/tests/TPTP/Veloci/LAT045-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL110-2.p.ma b/matita/tests/TPTP/Veloci/LCL110-2.p.ma index 1bc6a7ee4..9515feec6 100644 --- a/matita/tests/TPTP/Veloci/LCL110-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL112-2.p.ma b/matita/tests/TPTP/Veloci/LCL112-2.p.ma index 8c38afbd9..ef68697fe 100644 --- a/matita/tests/TPTP/Veloci/LCL112-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL113-2.p.ma b/matita/tests/TPTP/Veloci/LCL113-2.p.ma index 766232ffd..534c7fb7e 100644 --- a/matita/tests/TPTP/Veloci/LCL113-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL114-2.p.ma b/matita/tests/TPTP/Veloci/LCL114-2.p.ma index f71b12e57..2fce65768 100644 --- a/matita/tests/TPTP/Veloci/LCL114-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL115-2.p.ma b/matita/tests/TPTP/Veloci/LCL115-2.p.ma index 919437549..934852d6e 100644 --- a/matita/tests/TPTP/Veloci/LCL115-2.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL132-1.p.ma b/matita/tests/TPTP/Veloci/LCL132-1.p.ma index e69046020..f13905176 100644 --- a/matita/tests/TPTP/Veloci/LCL132-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL133-1.p.ma b/matita/tests/TPTP/Veloci/LCL133-1.p.ma index 4ed8eaa55..48138a19a 100644 --- a/matita/tests/TPTP/Veloci/LCL133-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL134-1.p.ma b/matita/tests/TPTP/Veloci/LCL134-1.p.ma index 4e8577400..96e607cea 100644 --- a/matita/tests/TPTP/Veloci/LCL134-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL135-1.p.ma b/matita/tests/TPTP/Veloci/LCL135-1.p.ma index 072bd65e8..1534861eb 100644 --- a/matita/tests/TPTP/Veloci/LCL135-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL139-1.p.ma b/matita/tests/TPTP/Veloci/LCL139-1.p.ma index cf69fbdd7..c05658d20 100644 --- a/matita/tests/TPTP/Veloci/LCL139-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL140-1.p.ma b/matita/tests/TPTP/Veloci/LCL140-1.p.ma index 6d42028e0..a134410a2 100644 --- a/matita/tests/TPTP/Veloci/LCL140-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL141-1.p.ma b/matita/tests/TPTP/Veloci/LCL141-1.p.ma index 45c5189c7..e70a70c3b 100644 --- a/matita/tests/TPTP/Veloci/LCL141-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL153-1.p.ma b/matita/tests/TPTP/Veloci/LCL153-1.p.ma index 87a148225..391936013 100644 --- a/matita/tests/TPTP/Veloci/LCL153-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL154-1.p.ma b/matita/tests/TPTP/Veloci/LCL154-1.p.ma index c4c03e265..4c0c98507 100644 --- a/matita/tests/TPTP/Veloci/LCL154-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL155-1.p.ma b/matita/tests/TPTP/Veloci/LCL155-1.p.ma index bf43acb83..71ed352dd 100644 --- a/matita/tests/TPTP/Veloci/LCL155-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL156-1.p.ma b/matita/tests/TPTP/Veloci/LCL156-1.p.ma index 83f8399f9..c01872fb9 100644 --- a/matita/tests/TPTP/Veloci/LCL156-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL157-1.p.ma b/matita/tests/TPTP/Veloci/LCL157-1.p.ma index d4cd09aed..e336e3a3a 100644 --- a/matita/tests/TPTP/Veloci/LCL157-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL158-1.p.ma b/matita/tests/TPTP/Veloci/LCL158-1.p.ma index 22f1826a9..ed138bd52 100644 --- a/matita/tests/TPTP/Veloci/LCL158-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL161-1.p.ma b/matita/tests/TPTP/Veloci/LCL161-1.p.ma index 6e86e46db..57fb55ec7 100644 --- a/matita/tests/TPTP/Veloci/LCL161-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LCL164-1.p.ma b/matita/tests/TPTP/Veloci/LCL164-1.p.ma index 1b7c4e285..a84605051 100644 --- a/matita/tests/TPTP/Veloci/LCL164-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LDA001-1.p.ma b/matita/tests/TPTP/Veloci/LDA001-1.p.ma index e5c9a4810..051af57e8 100644 --- a/matita/tests/TPTP/Veloci/LDA001-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/LDA007-3.p.ma b/matita/tests/TPTP/Veloci/LDA007-3.p.ma index c82d5ad14..11d43b6a2 100644 --- a/matita/tests/TPTP/Veloci/LDA007-3.p.ma +++ b/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/matita/tests/TPTP/Veloci/RNG007-4.p.ma b/matita/tests/TPTP/Veloci/RNG007-4.p.ma index a5656dbb8..e981ee5ba 100644 --- a/matita/tests/TPTP/Veloci/RNG007-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/RNG008-4.p.ma b/matita/tests/TPTP/Veloci/RNG008-4.p.ma index 90502489c..26341ce46 100644 --- a/matita/tests/TPTP/Veloci/RNG008-4.p.ma +++ b/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/matita/tests/TPTP/Veloci/RNG011-5.p.ma b/matita/tests/TPTP/Veloci/RNG011-5.p.ma index 249f09a22..fcf436713 100644 --- a/matita/tests/TPTP/Veloci/RNG011-5.p.ma +++ b/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/matita/tests/TPTP/Veloci/RNG023-6.p.ma b/matita/tests/TPTP/Veloci/RNG023-6.p.ma index e14e0768e..8397d426f 100644 --- a/matita/tests/TPTP/Veloci/RNG023-6.p.ma +++ b/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/matita/tests/TPTP/Veloci/RNG023-7.p.ma b/matita/tests/TPTP/Veloci/RNG023-7.p.ma index 2cc1a7536..01e94c6a7 100644 --- a/matita/tests/TPTP/Veloci/RNG023-7.p.ma +++ b/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/matita/tests/TPTP/Veloci/RNG024-6.p.ma b/matita/tests/TPTP/Veloci/RNG024-6.p.ma index 6a77615a3..3785a9204 100644 --- a/matita/tests/TPTP/Veloci/RNG024-6.p.ma +++ b/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/matita/tests/TPTP/Veloci/RNG024-7.p.ma b/matita/tests/TPTP/Veloci/RNG024-7.p.ma index 7b76445f4..135db3ff2 100644 --- a/matita/tests/TPTP/Veloci/RNG024-7.p.ma +++ b/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/matita/tests/TPTP/Veloci/ROB002-1.p.ma b/matita/tests/TPTP/Veloci/ROB002-1.p.ma index 9373a9bed..883467d61 100644 --- a/matita/tests/TPTP/Veloci/ROB002-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/ROB009-1.p.ma b/matita/tests/TPTP/Veloci/ROB009-1.p.ma index d4571bf7f..90f1c10c9 100644 --- a/matita/tests/TPTP/Veloci/ROB009-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/ROB010-1.p.ma b/matita/tests/TPTP/Veloci/ROB010-1.p.ma index 34f8df65a..765898668 100644 --- a/matita/tests/TPTP/Veloci/ROB010-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/ROB013-1.p.ma b/matita/tests/TPTP/Veloci/ROB013-1.p.ma index e8091c2ab..fe79d1550 100644 --- a/matita/tests/TPTP/Veloci/ROB013-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/ROB030-1.p.ma b/matita/tests/TPTP/Veloci/ROB030-1.p.ma index 6fac0285c..9868ec4d5 100644 --- a/matita/tests/TPTP/Veloci/ROB030-1.p.ma +++ b/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/matita/tests/TPTP/Veloci/SYN083-1.p.ma b/matita/tests/TPTP/Veloci/SYN083-1.p.ma index 0fcc15b76..1dc7202c9 100644 --- a/matita/tests/TPTP/Veloci/SYN083-1.p.ma +++ b/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.