From: Enrico Tassi Date: Tue, 3 Oct 2006 16:40:35 +0000 (+0000) Subject: reduced timeout to 100s X-Git-Tag: 0.4.95@7852~931 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a3cfb9758bac98014c32e88bdbc08f2c3bcd7a70;p=helm.git reduced timeout to 100s --- diff --git a/matita/tests/TPTP/Veloci/BOO001-1.p.ma b/matita/tests/TPTP/Veloci/BOO001-1.p.ma index 9d39e84b5..4cc2223d1 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=600. +auto 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 6014b9215..93b11c287 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=600. +auto 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 c8d225cd4..89dfcf314 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=600. +auto 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 dc59877b1..4ea34f1e0 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=600. +auto 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 05d7e3771..9542f452a 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=600. +auto 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 4e5de1bb0..c098b6cfb 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=600. +auto 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 287858022..04f83193c 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=600. +auto 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 b745d9d2b..0fd7e320c 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=600. +auto 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 2988e2077..4a04acbd9 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=600. +auto 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 1ed110056..3328ed780 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=600. +auto 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 f79df59b8..fd724a6a3 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=600. +auto 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 020cba1e4..8178f4043 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=600. +auto 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 792f4286f..764399c39 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=600. +auto 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 1108abdf6..94fafbca7 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=600. +auto 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 5cb02f22f..6451f3bd7 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=600. +auto 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 f7eba80f8..2823a4114 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=600. +auto 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 7e63ac0f6..bdd9c07e8 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=600. +auto 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 d3c76c275..202b96c7d 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=600. +auto 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 d8f58f5b9..2eab59e4f 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=600. +auto 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 acca29544..91aec5ae7 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=600. +auto 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 2563236c4..ba23e0205 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=600. +auto 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 78be71679..6d6f2ab06 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=600. +auto 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 722b41fd8..a1626bf6d 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=600. +auto 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 4b73d0bd0..123624d1b 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=600. +auto 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 9e14205a7..d76c4142c 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=600. +auto 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 0ac678c2c..1f399f862 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=600. +auto 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 fd5a87556..c2cf3ecbc 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=600. +auto 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 dd7560380..6154d8a34 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=600. +auto 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 0d67b7e8e..e8f9b3467 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=600. +auto 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 615defe7f..d8da7dbe8 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=600. +auto 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 8c6a371d2..5b38f0dd8 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=600. +auto 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 c3dd0be56..6ff4fddd1 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=600. +auto 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 0b1b928a1..2e179255d 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=600. +auto 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 11ce88f5b..d2cc7be9f 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=600. +auto 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 536efc4c7..5e84cf277 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=600. +auto 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 475f91453..e6db2d319 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=600. +auto 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 1881d33e9..4aca85e92 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=600. +auto 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 2332e16d7..144fac75b 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=600. +auto 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 4f68c0a2f..b8b90725b 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=600. +auto 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 d729fede4..0ade23762 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=600. +auto 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 2446698ac..7a21954e5 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=600. +auto 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 46f9219fa..724503625 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=600. +auto 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 6b3e51f8d..728762834 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=600. +auto 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 b3cd44dc1..662e3d7cd 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=600. +auto 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 7065d7f34..86a05a99b 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=600. +auto 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 e36faea33..f3e5b5d52 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=600. +auto 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 359d087d7..746e14da2 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=600. +auto 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 d3788ffb6..24ccd93b4 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=600. +auto 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 404a5f676..41779cae6 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=600. +auto 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 6b501576f..a59f55f4b 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=600. +auto 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 c6b265cba..b366a3f9f 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=600. +auto 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 441838a23..3734fb971 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=600. +auto 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 3731bf636..1857b0fba 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=600. +auto 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 c1976c2fc..fddb0328a 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=600. +auto 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 36b509452..6f4ebb664 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=600. +auto 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 37a0a46aa..636fa6b6d 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=600. +auto 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 e363b5da8..e60af56ce 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=600. +auto 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 7c3d328d4..a179cceba 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=600. +auto 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 8654fb42a..2d2bbc7c5 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=600. +auto 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 e4af9430b..9c6113ada 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=600. +auto 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 79cff6723..dd0f1ffbe 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=600. +auto 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 d913d5691..dfdc9b00d 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=600. +auto 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 b6e932463..f2cb5118f 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=600. +auto 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 132e4da8a..cc05447be 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=600. +auto 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 5169c5b4b..362338108 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=600. +auto 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 0002bc82b..02fbbcabb 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=600. +auto 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 e590c8575..a1c8dd0ab 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=600. +auto 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 fa64095fe..fe71489cf 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=600. +auto 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 29f5443fa..0f7c24aa0 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=600. +auto 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 da11b63b0..fcb3b6afd 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=600. +auto 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 34825a356..1011802d4 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=600. +auto 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 f792d143e..83be67ecf 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=600. +auto 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 eeee302cf..3bf8fe21a 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=600. +auto 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 87fbe746a..f97360370 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=600. +auto 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 7e34e0e2d..4e0da1e47 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=600. +auto 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 9c85e534c..afeda0d1f 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=600. +auto 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 d580276c4..773068e1f 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=600. +auto 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 34bc0c11f..e6bf5c0b2 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=600. +auto 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 8c7bfcc3c..e33eac2ac 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=600. +auto 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 478e1d333..562cd1811 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=600. +auto 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 0af6b7b0a..7736d1567 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=600. +auto 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 d4509fe67..f570845cd 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=600. +auto 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 a495736d9..6847c52b6 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=600. +auto 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 8aceda0c4..40442e00a 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=600. +auto 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 c06356f23..0727c7051 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=600. +auto 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 33a901d98..887c1ba02 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=600. +auto 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 5a0a95a43..3d19c2c02 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=600. +auto 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 3c53d6a42..bbce5c045 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=600. +auto 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 868dc50f8..ce184d7d1 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=600. +auto 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 6ebe28f69..bdbd3df36 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=600. +auto 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 a5be66a2f..bb79b6b40 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=600. +auto 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 7080776ff..d1f8a8f4e 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=600. +auto 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 3ed92317f..a657802e9 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=600. +auto 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 b046855ef..5fb6b6928 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=600. +auto 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 7e7269b0b..0212ea903 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=600. +auto 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 e11fa9e31..7531e2af3 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=600. +auto 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 29cb5dd90..0f55687c1 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=600. +auto 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 65a208272..98bb06522 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=600. +auto 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 bf2567579..f725b2f7b 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=600. +auto 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 0acd9c34d..90c11d85a 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=600. +auto 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 f5a68474f..383b0e2d1 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=600. +auto 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 dc8c068b3..29a70eadc 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=600. +auto 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 c19277687..03ee7c53f 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=600. +auto 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 0da9490b6..e6fc69f78 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=600. +auto 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 82f45ad90..18243968e 100644 --- a/matita/tests/TPTP/Veloci/GRP168-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP168-1.p.ma @@ -116,7 +116,7 @@ theorem prove_p01a: \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply (inverse c) (multiply a c)) (multiply (inverse c) (multiply b c))) (multiply (inverse c) (multiply b c)) . intros. -auto paramodulation timeout=600. +auto 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 bba04f4f1..bcf26d5d9 100644 --- a/matita/tests/TPTP/Veloci/GRP168-2.p.ma +++ b/matita/tests/TPTP/Veloci/GRP168-2.p.ma @@ -114,7 +114,7 @@ theorem prove_p01b: \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (multiply (inverse c) (multiply a c)) (multiply (inverse c) (multiply b c))) (multiply (inverse c) (multiply a c)) . intros. -auto paramodulation timeout=600. +auto 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 19233ea8c..849057bc5 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=600. +auto 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 cd9b1ecfd..076784ef8 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=600. +auto 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 5b04b0b96..b67193505 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=600. +auto 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 3f3813077..33d15dcc3 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=600. +auto 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 8641d997e..3b13987b5 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=600. +auto 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 1f93eda30..59f725c19 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=600. +auto 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 558e029c1..4c890fbd1 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=600. +auto 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 43b241485..1942f7064 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=600. +auto 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 615fcd9a6..a358b5fd3 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=600. +auto 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 b24baebf9..aac5c99e7 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=600. +auto 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 d22324e7d..a4142e5c9 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=600. +auto 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 b9a448f24..043fc5af7 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=600. +auto 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 d87f2d141..47d76e5e2 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=600. +auto 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 190ce115f..7d8396675 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=600. +auto 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 9a4fcec59..cbfcff30c 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=600. +auto 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 b19e7973a..62ad0624c 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=600. +auto 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 12dc8c91a..9281a270a 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=600. +auto 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 dfc9a818c..ef2028982 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=600. +auto 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 5b46051a1..1804cdb78 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=600. +auto 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 b8bc4380f..fcba4e4e7 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=600. +auto 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 716d8e2bd..3d782b025 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=600. +auto 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 6b31ac48c..3ade69780 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=600. +auto 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 908ea3c47..6413b5743 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=600. +auto 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 76d709891..6bf794240 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=600. +auto 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 c4cb419af..2ebeb9f5d 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=600. +auto 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 c4c633afe..c4eaf5861 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=600. +auto 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 8a6ef3a3e..b673ea1fe 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=600. +auto 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 b2c04b8bc..21831160b 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=600. +auto 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 5d40fea5d..264794f50 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=600. +auto 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 3004ed9c1..51a728493 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=600. +auto 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 744734796..0026f5c89 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=600. +auto 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 2ff23a7b1..fe07b798d 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=600. +auto 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 836a3ad5b..600af87e1 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=600. +auto 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 89c4207b4..921714afd 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=600. +auto 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 63a8d5909..8963ddaf8 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=600. +auto 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 6bbae9cb2..0e280132b 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=600. +auto 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 4dec7d562..af079e663 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=600. +auto 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 1df419c49..d655496c5 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=600. +auto 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 ded973ff3..a7d1d5a8e 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=600. +auto 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 626cd7484..e26c08db4 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=600. +auto 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 586e03aa5..0458df1fa 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=600. +auto 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 11bd0b244..146e6a814 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=600. +auto 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 71dae36ec..466126222 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=600. +auto 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 23121a3dd..e78bed00f 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=600. +auto 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 81534b301..fdf42d748 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=600. +auto 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 70ac86f23..74dc8a63a 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=600. +auto 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 fc49b2076..83eb4b753 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=600. +auto 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 da708344e..dde992a18 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=600. +auto 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 bbbb368c8..ee9bff2fc 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=600. +auto 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 0209207e1..6ff2950a6 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=600. +auto 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 c5fd793c6..33f0bd79a 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=600. +auto 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 3fa88b862..ab4a50104 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=600. +auto 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 21eb32dd1..37900e2ec 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=600. +auto 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 2a772c9e6..efe72032b 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=600. +auto 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 38a6ac6c3..66b15a5cf 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=600. +auto 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 6d3230bdb..1e66b6585 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=600. +auto 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 c08fc153a..bc5433839 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=600. +auto 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 44086b165..5256be724 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=600. +auto 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 ab4ad4c2d..91748c17f 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=600. +auto 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 efcfc9f21..eb94e08e2 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=600. +auto 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 d02e348ee..69d89ee91 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=600. +auto 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 ca2631827..77abdbeea 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=600. +auto 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 bb79a3b0f..f04d0b10c 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=600. +auto 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 77f2537c6..f9dbfb85e 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=600. +auto 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 a2cc53bc7..09e45674e 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=600. +auto 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 d683744ff..e411b5724 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=600. +auto 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 e64a752dc..396c9dd37 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=600. +auto 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 6b5ac4a2a..0a2a60ff2 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=600. +auto 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 467c25cac..df8fe3ff8 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=600. +auto 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 190874f56..5a76d9981 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=600. +auto 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 dd2e955db..b647dce22 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=600. +auto 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 d914e6b24..cf0a795d9 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=600. +auto 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 cfddf6670..16cd566aa 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=600. +auto 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 e919cd310..118437264 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=600. +auto 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 5d1418cbc..9720c564a 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=600. +auto 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 14f0155ad..f740a647f 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=600. +auto 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 53f1956a6..760a12564 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=600. +auto 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 bccea6094..1f6da909a 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=600. +auto 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 4cbe988a8..0f9ec0dbb 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=600. +auto 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 3bab0d3b1..418921649 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=600. +auto 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 1e4e99e7d..e44ea55db 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=600. +auto 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 b05d41157..c37de12c2 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=600. +auto 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 a85c49cfe..ccaa5e80e 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=600. +auto 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 3ece06e99..74691ad6d 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=600. +auto 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 134e7897f..a82d60e88 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=600. +auto 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 24ddd7e3d..e743542a3 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=600. +auto 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 f91a42464..5b2a189ec 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=600. +auto 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 f27de51d0..66ef7c555 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=600. +auto 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 881af350a..c89d13252 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=600. +auto 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 8508efdc8..0e9eac474 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=600. +auto 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 b30ce397a..354515802 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=600. +auto 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 8d358e351..9def73c5f 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=600. +auto 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 03160a58c..dd33c8ed7 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=600. +auto 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 d0e3599f7..06dfd2c5e 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=600. +auto 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 9ccd994e9..1305cf6ce 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=600. +auto 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 de36114c9..965637bc7 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=600. +auto 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 4e19411a9..19b676eca 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=600. +auto 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 9d72d695c..3c25c6ffe 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=600. +auto 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 4693754cd..5b583615e 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=600. +auto 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 7a6ff4119..e637e7d4a 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=600. +auto 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 a317d5a15..6f271dd69 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=600. +auto 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 d64555fdc..77eef1f73 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=600. +auto 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 61b2a8020..c2656bf79 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=600. +auto 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 290d935a0..6bf34a806 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=600. +auto 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 d1a988c93..15eeca809 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=600. +auto 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 e1cc77b66..ee30724b2 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=600. +auto 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 c68f5a3bb..413d5d0d0 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=600. +auto 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 e1f6f5844..c9075f2e3 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=600. +auto 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 de8d77760..ba2e724eb 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=600. +auto 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 098aff381..548df9d84 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=600. +auto 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 d9727fe90..570d23724 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=600. +auto 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 17b66a72f..05e4b3cfd 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=600. +auto 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 b37752561..ea3be43e0 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=600. +auto 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 6c05f2e05..e2a7df884 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=600. +auto 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 d9a5f5c07..1bc6a7ee4 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=600. +auto 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 76e8e97aa..8c38afbd9 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=600. +auto 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 672763240..766232ffd 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=600. +auto 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 a92adbdd7..f71b12e57 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=600. +auto 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 38a627df9..919437549 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=600. +auto 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 07a4b2598..e69046020 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=600. +auto 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 56c0f69a4..4ed8eaa55 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=600. +auto 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 cd72ff7ee..4e8577400 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=600. +auto 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 828dfc8ab..072bd65e8 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=600. +auto 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 addf036aa..cf69fbdd7 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=600. +auto 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 47e7f8f0e..6d42028e0 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=600. +auto 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 8e45dc567..45c5189c7 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=600. +auto 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 e09864dac..87a148225 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=600. +auto 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 6a7895e1c..c4c03e265 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=600. +auto 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 9cc37832a..bf43acb83 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=600. +auto 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 a71e12788..83f8399f9 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=600. +auto 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 04ec616b7..d4cd09aed 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=600. +auto 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 445fca829..22f1826a9 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=600. +auto 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 7504ce588..6e86e46db 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=600. +auto 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 38d3ab4c5..1b7c4e285 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=600. +auto 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 d75a6d96e..e5c9a4810 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=600. +auto 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 ea2608643..c82d5ad14 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=600. +auto 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 644471972..a5656dbb8 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=600. +auto 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 f3f5e7595..90502489c 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=600. +auto 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 3d08d1bcd..249f09a22 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=600. +auto 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 d3f15e917..e14e0768e 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=600. +auto 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 e5f87cd21..2cc1a7536 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=600. +auto 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 806f1bdc4..6a77615a3 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=600. +auto 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 4b535916e..7b76445f4 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=600. +auto 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 26ad55903..9373a9bed 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=600. +auto 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 58208932b..d4571bf7f 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=600. +auto 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 95c6389c9..34f8df65a 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=600. +auto 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 681780731..e8091c2ab 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=600. +auto 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 4dc584bd3..6fac0285c 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=600. +auto 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 46a932900..0fcc15b76 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=600. +auto paramodulation timeout=100. try assumption. print proofterm. qed.