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 9d39e84b5c470f7d88abf0cfa9965503cbe8455b..4cc2223d110f70c9d265113ba78733e1a3667168 100644 (file)
--- 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 6014b921522c33c08d5c2ea9da85321ee74ca52f..93b11c287d87b6a7f34c18064bcade604e099d2e 100644 (file)
--- 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 c8d225cd4fccdf33c574103039530cde94988f6d..89dfcf3149887b8dc3433b2362f6cc310d41af7b 100644 (file)
--- 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 dc59877b1f9c4265f83ce97bffe3bbb72368d41b..4ea34f1e01624a6cc0b14702a420f500ad4915de 100644 (file)
--- 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 05d7e37716bb43a9e90b8ae7f6f2f483d8aa8ade..9542f452a830ecd06856b4bb031d1ba0d8d14c3d 100644 (file)
--- 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 4e5de1bb073437ce692c49bde64cfa41af400ece..c098b6cfb1965e8e09c98916f27aaaa8651cc317 100644 (file)
--- 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 2878580229fb3418e52d0d880e9781f092ed224d..04f83193c4682e705fc7664a35debddf5f007ffa 100644 (file)
--- 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 b745d9d2bccd2eebf684d6ad27164fd4e8a82b74..0fd7e320c03679309c4e6c96e7bef1f00f9a8dce 100644 (file)
--- 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 2988e2077ff6ccf57dcd3ab81ecfced07affdf74..4a04acbd956d02d1431886baac30b5deba542083 100644 (file)
--- 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 1ed1100562082e6372c156d271f9408f8c09e7be..3328ed780e7c6b913c7980629b5e961524e92efd 100644 (file)
--- 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 f79df59b8864bf2095b74cd8bf734acb55373018..fd724a6a3f7d609658319c76b85a95a7d7d2b9f8 100644 (file)
--- 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 020cba1e4f24ccb1870d87a4eaaaf74580030b9f..8178f40434bc665bbe98b56c95135921ea00073a 100644 (file)
--- 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 792f4286f3badb25d5f0eae0ab01c9c18b76499c..764399c396a4c9aaa193616b21a809e1d5681a4c 100644 (file)
--- 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 1108abdf6fa41ea3b9307b9b2040af14acd9310b..94fafbca736ba1861d87ae9ddf67a0fab5e63d6b 100644 (file)
--- 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 5cb02f22f6e6eee7a603782958d043a5b54a02bb..6451f3bd7b0beb8e2a867e9d54f93867b0bac5fe 100644 (file)
--- 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 f7eba80f847ed9b882b5fee58d0cdc5e20e19b48..2823a41140a01db13744d72c006605240b943e8b 100644 (file)
--- 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 7e63ac0f6a15912044e72c3e5b6d0b59235ceafa..bdd9c07e8d4f50764f8d588a25258ce70fbeac93 100644 (file)
--- 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 d3c76c2751d3c45839cceaa94393395c14519219..202b96c7d7e9fce0953606570d3985cfb3ea78ef 100644 (file)
--- 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 d8f58f5b91f0e51d36bfdfbc9209a0d1a4a91f90..2eab59e4fbc24fde8ec3e28e61119393b05cbaf3 100644 (file)
--- 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 acca2954452e53c2242a4df75c3501ceaf5626c5..91aec5ae7b363e46a1ca76bf2f793d140dadfac6 100644 (file)
--- 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 2563236c48dc2c2f09ddf1d93609247807c175c1..ba23e0205acfe62ca30aeca2c39b0b131e14337c 100644 (file)
--- 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 78be716799dadb3aa3586e1aca656c39b4db2d32..6d6f2ab0661732c17b223b34038ea2583918b85b 100644 (file)
--- 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 722b41fd8ac14d8d65e24e5e0df7aaa0ea0ae125..a1626bf6d9325eade289b397e29943d1194ff0ac 100644 (file)
--- 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 4b73d0bd0896888b5bdf88a4918db95fef416811..123624d1bd09d93ff37cac8588aa46564ee26b4d 100644 (file)
--- 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 9e14205a7fd90cf2e30fa7021ecad174e4c5ab3a..d76c4142ce60fc1f6cb41aafe3e89bdff8543397 100644 (file)
--- 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 0ac678c2caaa5791138e82f84fc6415bdc0cebda..1f399f86220471c2e3640bcdb586d71a8c3585e9 100644 (file)
--- 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 fd5a875566a537a548dd3cc4beb80ab43e3a72c2..c2cf3ecbc486cda0e091fedd896c652e0318f629 100644 (file)
--- 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 dd75603800ae22c419967862e7652bc2e59eb08b..6154d8a34ca4550b30ef47c34491190fa6157ed8 100644 (file)
--- 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 0d67b7e8e390eb06d180e3cd1707da237af3db2d..e8f9b346725afdc352175278e0828063db206856 100644 (file)
--- 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 615defe7f04f6bbe8da6010c6233fc3e18384180..d8da7dbe8ed72f57802e44758a798bc2f2397fe6 100644 (file)
--- 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 8c6a371d2d14c54fe7c3771dd4a96516fd12f4cc..5b38f0dd823ad64cef45f3f4ad489958d6205a03 100644 (file)
--- 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 c3dd0be568d685ecb30b01a59797ed7216ddd6f7..6ff4fddd1dee4405db0001343c74dab9811f6b13 100644 (file)
--- 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 0b1b928a12f99e64d9cd1bcd3d9e1fe3809b64c0..2e179255d44c10601a5cb53c83b4898858d360be 100644 (file)
--- 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 11ce88f5be3e15a793fd0e4d3efd3d71947882c9..d2cc7be9fc92de48be6e1992076791be556c035b 100644 (file)
--- 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 536efc4c7fec14a736e2d6407520ffe78b637540..5e84cf2771b49e43b052803bcbe0438e5626fffe 100644 (file)
--- 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 475f9145362a2e5b9a1811810926bd6a76fd35f2..e6db2d319974b7c86e400de9c69d50834785b0e1 100644 (file)
--- 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 1881d33e9d381ea2dac5c2b9dddc4cdf0e5f5022..4aca85e92410d7c3d27b31485f4198301b9bc8a8 100644 (file)
--- 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 2332e16d7d071fe858942d170be6e3db9cfff109..144fac75baa5e964c31ce4dc40b4aa6a8c64dfcf 100644 (file)
--- 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 4f68c0a2f16a86cdea6828831a8eb6d890738933..b8b90725bbe50a51909fe37dffe80a9ba95ee492 100644 (file)
--- 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 d729fede4fc0f3abb520ef6d8ab830c404dada9f..0ade23762faa026f01e6649c1ad0d448c99c013f 100644 (file)
--- 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 2446698acecfce2a362e51e94c2334d996cfad2a..7a21954e57840dfaf27f067e98e652d858082c50 100644 (file)
--- 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 46f9219fa4a996683308c896dcf81fa8a8ae1b32..724503625bb679fa5a967bdbb5cbb5862b16561f 100644 (file)
--- 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 6b3e51f8d6fd8b53741b7e46148caf886ba9995c..728762834a4910a16904411ae18efe8127efc7f1 100644 (file)
--- 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 b3cd44dc1abaffc649a05cb547b50efa16cc4801..662e3d7cd0782d990f5c3791106337db465e9950 100644 (file)
--- 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 7065d7f3432dda52a5f4a9c09d5861edc0e452fa..86a05a99bf51b3a31016e2d727684e54a17f21c8 100644 (file)
--- 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 e36faea3324c1dc8e9d7660221f199cab7555127..f3e5b5d5221f91b2e1178c60fd33c7abb23cdbd2 100644 (file)
--- 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 359d087d77e8af7ae1cf5a758d961bfd5f13c90e..746e14da2a0f24a62e0aaed910620c9d3e04a057 100644 (file)
--- 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 d3788ffb62ae2fda05241f561b8417820e70a853..24ccd93b498461492c954837fbac4e0e38d7b6c9 100644 (file)
--- 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 404a5f676b522c6a4c22c17b13f7a8e42496b892..41779cae6bbf4caff1578e1aee5fc54131b0496d 100644 (file)
--- 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 6b501576f6c4a32a7345cbb43b451635cd4e16e5..a59f55f4b5b7fc83dbe0ed07a94047a3f63d9d3e 100644 (file)
--- 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 c6b265cbaef22995c8d3309d22d9640794a3fc3c..b366a3f9f7e1e209f34121e8cbde6e7b8ad9d0fc 100644 (file)
--- 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 441838a238f441bfacb9970ae9230b5b01b5961a..3734fb97180239b01706d2bd91dcc6ed06a647ca 100644 (file)
--- 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 3731bf636679490d9340616e094b8e8714c8dd76..1857b0fbaba86854f6486b6ce3910acb371fb63a 100644 (file)
--- 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 c1976c2fcbb96e84d786b4bd4b1e744e958d6860..fddb0328a780afeda189ea9962547f02621ba705 100644 (file)
--- 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 36b509452659726d1ef02d46f570c29598589319..6f4ebb66470a30ec2263c90aa334d552d01a7a95 100644 (file)
--- 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 37a0a46aa9f27522c74b0a692c0bc239cd284718..636fa6b6db88b2290173c5e224c0f2e33ab37330 100644 (file)
--- 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 e363b5da8b32262e2d5ed8aae161aaf49186ce9e..e60af56ceff98ff7d3ca1e9e8e1c21f3586027f4 100644 (file)
--- 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 7c3d328d455e1a2d27b15c0d6ce9b889f1df6941..a179ccebad2b6b0eb9dd3fc1bd3ef84ee123f4c6 100644 (file)
--- 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 8654fb42a249b2b7526b5e616fe61acef6d7d910..2d2bbc7c53807ffc400fa89539d90f670bdb3731 100644 (file)
--- 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 e4af9430b6b97733f62ebfed3c12e5fd91daca8c..9c6113adaf432be0f43ff5ae21286a1948525625 100644 (file)
--- 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 79cff6723c446fcac5d3441756e6352d89892c01..dd0f1ffbeb4bf8f2e461dc75c3dd87c6c836e69c 100644 (file)
--- 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 d913d56910a6c3884160d9c9f25100731cdf4bda..dfdc9b00deba455d4da47a0e88983d6c3b3ea41d 100644 (file)
--- 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 b6e9324634bf746ee680fce29df76016462f19c1..f2cb5118ffc461e3317b48aeaa8160f4fce28003 100644 (file)
--- 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 132e4da8a0e1961fda2d55e4ff37060e0f23ecdb..cc05447be0f8d2df6f149b762cf357f2fef992da 100644 (file)
--- 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 5169c5b4b17d2bfcfb0daf6fb3dd9a11891b5686..36233810860966d7595a527dff10e0d982ee71c8 100644 (file)
--- 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 0002bc82b16756f54bd7597211a62ce2f577bb3a..02fbbcabbab97d7fd3b7c39d42b5a863f2f61c17 100644 (file)
--- 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 e590c8575671936346997222a69dd2da8bb4cb45..a1c8dd0abbc1b33aac8af66abfd07bcc4f459b2e 100644 (file)
--- 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 fa64095fe0d3e363014fce1e7cdc2b0b3cec5e52..fe71489cf369f52b910c8f556811d520a9bc1744 100644 (file)
--- 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 29f5443fa6b101f645eb664b234a7b39021967bf..0f7c24aa0dfd705bf664a91ac840e75b269cbc8d 100644 (file)
--- 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 da11b63b08defaaf69da057f5835e0523c6bee22..fcb3b6afd38e2b299a28b60cbcca4f7972124451 100644 (file)
--- 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 34825a356b0c585dfdecf2bb9952a34524ee4084..1011802d4ddc1a62d2f7becff087e90604c8ea80 100644 (file)
--- 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 f792d143e13627cdc4af98a3d33ec18d20575d96..83be67ecfd4c385f07397b11de764e6e1f2b5b79 100644 (file)
--- 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 eeee302cf85a275e53090b68bcdf443f2280b62f..3bf8fe21ae1b3eb2af325bf9e9cf28b5605de3f1 100644 (file)
--- 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 87fbe746aea71a51137755270a3951553889392f..f97360370f53f2062f761ed0244481d3e586d86f 100644 (file)
--- 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 7e34e0e2d1fafc6c219b1d21ee11380f5ab10548..4e0da1e47d95eae0da970c2e0f9a49f41d5684ac 100644 (file)
--- 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 9c85e534cd42eea3c552a4a19104ba181daa0c21..afeda0d1fbeccbad17291200457a4e1c687507c2 100644 (file)
--- 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 d580276c4939c14b10116aa57b78eeff9c679b6c..773068e1f4d7f084931c700fd16a68dbe328b583 100644 (file)
--- 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 34bc0c11f78eee7b012300bebe5f20d62c3a78d5..e6bf5c0b28a5c4f2806c53dde4199420124aea9f 100644 (file)
--- 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 8c7bfcc3c82001d9c67cf4db85bc86e8d7b6d897..e33eac2ac9a898e2ae63c8a9ec83fb66cc827c1e 100644 (file)
--- 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 478e1d3339adee00fac6d30d6448753f218a11ab..562cd181147582543a900d0239140d9aa2963f7d 100644 (file)
--- 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 0af6b7b0a0c9d92b3ffc3a20d8a00a92007426c2..7736d1567b95f01cf33a6408b3861f5ee8a0573c 100644 (file)
--- 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 d4509fe6799c6d879c2b9c2089312c4c60b50798..f570845cdef12b4b6ae02a95d9781caef8450a94 100644 (file)
--- 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 a495736d95a35986ba3d790be2d3930afed890d3..6847c52b6986d6d1c8653d378882066c3cc33a9b 100644 (file)
--- 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 8aceda0c43c4514a14c53f98093496c30327055e..40442e00ae9eb333d1d4b0de395dd8ad0abbdcaa 100644 (file)
--- 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 c06356f2311bc0c992348a23ea89854dae47e38f..0727c7051ccc90990566d9ae56368ec870cb0b15 100644 (file)
--- 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 33a901d9807b186deaee576ed576526ae9a76669..887c1ba02b7baf6e9a5b5e605066b3e8a658feb2 100644 (file)
--- 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 5a0a95a43a975f2573cb3e74448aab3da8f000ce..3d19c2c0274fcfe968e744dc91acc8eeea7cddc5 100644 (file)
--- 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 3c53d6a42b82f5c92b62fac82f5995cf697f217b..bbce5c045bb709889f7c0f004616332eee4d4787 100644 (file)
--- 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 868dc50f8e7f2daf35d732919378fffccd1d4d42..ce184d7d14b527903305cde399c9c30143ae0a8d 100644 (file)
--- 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 6ebe28f69ad8d2f9e7eb94f498343c988d7c94a0..bdbd3df361008b8fd2515f9344f38a5b4823730b 100644 (file)
--- 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 a5be66a2f2a1ae8e046ff23d59c726965b535b43..bb79b6b400a04385c43846f8733ddbdd08de4892 100644 (file)
--- 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 7080776ff82de90ade9ca6df3b1c9b50daef37b6..d1f8a8f4e5376a0271599ae088ed5b53114636b4 100644 (file)
--- 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 3ed92317ffae0513671b7a490c33e510c28c492b..a657802e9877fb657aab02094083ff9c4aa09c39 100644 (file)
--- 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 b046855efb5c0e1b3e8b9d418c98b367d665de1e..5fb6b69282f615ef2954cfb2c40f1d2bd2b7088e 100644 (file)
--- 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 7e7269b0bad58b44eadab1bce4c50db787d0b997..0212ea9038a9d543037a7b12036e997ec965eaba 100644 (file)
--- 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 e11fa9e3163c22c04f1db4e1764c609d2ef0cae3..7531e2af3926075aa6fca2147d49f33cff640cdd 100644 (file)
--- 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 29cb5dd906ba1bd6a0aa438212a5a5057c8391dc..0f55687c183ef7ff25bebc47ddbaabf85036efc9 100644 (file)
--- 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 65a2082724606027c004916a404b7e020cb9c629..98bb065228cb64469fee32dd6262802c583b1b5d 100644 (file)
--- 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 bf25675792928da2beeb4fcc8494300d103d79ca..f725b2f7b760d5ccce8d79a014d3128ab0557f12 100644 (file)
--- 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 0acd9c34ddade69411bb7dd0fed41cf51cc6b2e0..90c11d85a4fdbb73558e2e726d0782fe78426874 100644 (file)
--- 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 f5a68474f9d360c2c4030dc8b6349510bffcbcd8..383b0e2d10f58c5a1b3dcdb8c454d340948e1dad 100644 (file)
--- 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 dc8c068b328060e98383ae5a6a739c4d21775e1c..29a70eadcb1100b966fdbce861c014945be58efc 100644 (file)
--- 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 c1927768729043293b2f2056d5a79af549a28ccb..03ee7c53f9024302afa2b5d26b66d9362b54cf17 100644 (file)
--- 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 0da9490b6425a3b028b9e77ac8f90d7a9491da27..e6fc69f78c792d63a1c477cb7b7f7258c377cc91 100644 (file)
--- 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 82f45ad9083c12e37e9e4084a18f094adc35cb1e..18243968e41ee32f6a76d21fbdd3a5b8216023aa 100644 (file)
--- 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 bba04f4f1138c551c5e5490418be4bb5a4d3862f..bcf26d5d95399270d42dd2280a1cbd6ec703a5ec 100644 (file)
--- 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 19233ea8c55cbf52c03ffe9063234df47762fd23..849057bc54e2faf3dc646debd38a9b41ed257ab6 100644 (file)
--- 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 cd9b1ecfd67cd72aaf440c905ee2fa90e03e3474..076784ef82708fc2d5bcec15e0e7fbe12a8b47b6 100644 (file)
--- 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 5b04b0b9644ab08397a9e0a5d76a8679a1dafa1b..b67193505fb031ae12bda1e43040bf97c04554e3 100644 (file)
--- 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 3f38130770365f478c17cccac1cca9515d0dc71a..33d15dcc3effc6c617f81ea0e5762f586c8e74d6 100644 (file)
--- 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 8641d997e4d11195556b8e04f8119b345a5054af..3b13987b5c6b457c6faba669cc9f76e5adbb7310 100644 (file)
--- 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 1f93eda305c5cfa27900287f576444f5bab6927f..59f725c19e43cc3df43b2cb47f9e758fea1db076 100644 (file)
--- 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 558e029c1df77613f863cb51c5718dee46e80dd2..4c890fbd175c13c180d53cfc16ee8d913d9dcd40 100644 (file)
--- 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 43b24148526511d8fcc55b2b6b3a2422419d5198..1942f7064097a84600e6e6bc0ff3b1deeeb2f038 100644 (file)
--- 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 615fcd9a67f972cffada959a975358416b48eef1..a358b5fd3bd52441e1847fa96759b50f3b38ee41 100644 (file)
--- 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 b24baebf99831e8bb770fe3023596b9e36d58537..aac5c99e71c5998fa1f17910f653e592a6a4d2b7 100644 (file)
--- 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 d22324e7de248bfd89f6abd902bd8ef5a5ea8b3e..a4142e5c94c6c4373eeb28b12723911e75ea3621 100644 (file)
--- 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 b9a448f24e9e4a92f2a52fa84f549c77a019c4a7..043fc5af7c90c055a464c78cb3d00e67ce6490f9 100644 (file)
--- 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 d87f2d1419780a6696f0235f096785ee41d5f219..47d76e5e258d3fa0979397d271a80718d207a1f4 100644 (file)
--- 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 190ce115f69e7645a998a147b4b73e2e7493ff9c..7d83966759574459a810d258decfeef6192bf59d 100644 (file)
--- 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 9a4fcec59cd3cd22a5154b37b0472bd71cc55c17..cbfcff30c07528dec7cb5db5b600a1498b2954a0 100644 (file)
--- 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 b19e7973aa8fbfd65cdf8a1ac89e2bc0ef6a07c2..62ad0624cee90f5b298a7ad01895f4435e0af508 100644 (file)
--- 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 12dc8c91a39048a00b2609b9c69360ed5c1e04c4..9281a270ae34b5113728ccd27077c589826a4c7c 100644 (file)
--- 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 dfc9a818c3e571a2260359cfb5580643a206d3ad..ef2028982032601a18700b97016393600b972f1c 100644 (file)
--- 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 5b46051a115bb10c521c7a971607d3e4dce49687..1804cdb7806294c3914faae4ca9bb62bc7c14eed 100644 (file)
--- 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 b8bc4380f608e7e2aff6f5dd612e028606993794..fcba4e4e7be7f2da215e5874938a556490a9c495 100644 (file)
--- 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 716d8e2bd295830025624a5c32df063a34dc2a7a..3d782b025a9bccd2c7f61a30dd476d985ab402b9 100644 (file)
--- 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 6b31ac48c8f2f5588cb80f6f7eeb5a5391e1f1d6..3ade697807165137cd4cb230404310cad2419c36 100644 (file)
--- 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 908ea3c479679febe041ef64ee2b7f3efdbd53ee..6413b57436b0c335d1f20d240156426ab1a8a625 100644 (file)
--- 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 76d709891757e19b45f978c28432506f84c4dc7e..6bf79424052646fdaa2721d97628702c57fd947e 100644 (file)
--- 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 c4cb419af308483302c36c3a051028c07c056fa2..2ebeb9f5d11b2f26eb2e4abc1cfce0a769f8f3a5 100644 (file)
--- 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 c4c633afefcb47df72dda567d09ca2b3e8ad77f4..c4eaf586110e166ccdce790307e96873a6b57b1b 100644 (file)
--- 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 8a6ef3a3e49b6f116dc021701c1753912cd66e38..b673ea1fe23a08a0b3918f45b37257e28b13b8a6 100644 (file)
--- 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 b2c04b8bc056b4b855f1671be7b96ea6a11bebee..21831160b07a52757bb343f3916649468647553e 100644 (file)
--- 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 5d40fea5d356e39d71f361689a3766f4a5f96887..264794f5095e6b0d43030c32ab3068750f5095be 100644 (file)
--- 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 3004ed9c1a6ac5c4a855f524be2bd2ba2b8948a1..51a728493f532e3fe019ba4c70f679c7fde27b10 100644 (file)
--- 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 7447347962d549d3fac5d9b9043339a1e9f8ece8..0026f5c894124afad4facd1396b539065dd5aa44 100644 (file)
--- 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 2ff23a7b1b0f32341dc73fa762cec231017c2982..fe07b798dd04b16a952f5e6240b15883d85faa3c 100644 (file)
--- 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 836a3ad5be6c9f2eac10b05eef4dd2a7a3f0be20..600af87e1ed5154f91b023c3ce4e14cd70bf9eac 100644 (file)
--- 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 89c4207b4881e9b67001b36bb2bd63ac8a57eb5c..921714afd8d5802d41186134bcc80f6f919dccbd 100644 (file)
--- 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 63a8d5909b92bf95aabb1a3c6eff34940554bfff..8963ddaf8c14bba1bbb5c1bf201ac222784b12ae 100644 (file)
--- 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 6bbae9cb2596041dac35ebf6e13ebe7c6f02437f..0e280132b5812d2cb7be19cd8641ef5662cf5442 100644 (file)
--- 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 4dec7d56264f38e5dea499506276eb05599b7e91..af079e663ea86e0e5cccdea20f343b861dd9a8f5 100644 (file)
--- 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 1df419c495131e1f93e769505be1a84b17001310..d655496c5a7b95234d59ae884ecb19487f9747a3 100644 (file)
--- 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 ded973ff3bfa61225788e2076a577b8de0e741ec..a7d1d5a8eed7a1e903e0de5fcd28d061198a7503 100644 (file)
--- 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 626cd74844b29e9597b6168fe10368b73c5bc157..e26c08db4e3f407cfb2ee0078ab6d91798c675f8 100644 (file)
--- 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 586e03aa53054a3618b7c1c06a32d864a76631a6..0458df1fab5df73bfc2c04b515bffe2d03a9753a 100644 (file)
--- 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 11bd0b2445394b7cc1e556a3959c2d1f880f9054..146e6a8141932c3b219b1f6ec872bcdb49588375 100644 (file)
--- 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 71dae36ec36c63b12f775e958618a7a56bb0463c..466126222903977608cdab6cde51ad70a7535802 100644 (file)
--- 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 23121a3ddcf1396263bc24029ac1f4f16e0cf206..e78bed00fb5f380785cceaf18fd758be001331e5 100644 (file)
--- 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 81534b301753a985f183fdad4cca78b7a0c7f5ca..fdf42d7482fbf94d8176f055e6e8e2d3de830d63 100644 (file)
--- 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 70ac86f237a3809fcb5bb43ab01cf5f11515f9b7..74dc8a63a312f584cdb10222a59219dc40a15c28 100644 (file)
--- 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 fc49b2076a7da24b8828f72c3bca81c58462ef39..83eb4b753ff39076281bfd1d204a48fdbb49e811 100644 (file)
--- 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 da708344e2ab71e9ee995e1089d3f794e37406a1..dde992a18be11a2553064a53aee52ec94a05327e 100644 (file)
--- 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 bbbb368c874dde61aaa585cf7f2cb1b1ed48df91..ee9bff2fc5e764654976c5fd72f49937992fe076 100644 (file)
--- 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 0209207e193634917320513ece872eac70ebc751..6ff2950a60a8cb9655d4d8e3900a5a2fab6dec36 100644 (file)
--- 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 c5fd793c672bc5e048aaba5766e85393bbe20db1..33f0bd79af30580fac1b799a500bb88e79ee4893 100644 (file)
--- 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 3fa88b8629de98349d6f8c4bbbb987235cba77d3..ab4a5010442ad01b08c5112c449739719c8105f0 100644 (file)
--- 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 21eb32dd1cce1d96b596d6e25f0dfea6b59951a1..37900e2ec9452e89b8bdcc99d77a80c146240e43 100644 (file)
--- 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 2a772c9e658ab30e8637c5e167a29d802c4f6f40..efe72032bc7eb19bf7480fedd97cc837d85b576e 100644 (file)
--- 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 38a6ac6c3efb9c77356f4bb5c21945c601bab95b..66b15a5cfb001f90d4b5a90bb9660d86075d4185 100644 (file)
--- 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 6d3230bdb7bbc336ecf88c5e995ccba474122d9b..1e66b6585a6feb9be4f167ed9db945ca3d5ce754 100644 (file)
--- 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 c08fc153ad65ed336a1543ca7ee446261e4114cf..bc5433839ccbef7000d6fd1e167a365660f5239f 100644 (file)
--- 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 44086b1651f3fcb8da12bb1941b6b505884da6e3..5256be7249b1df2a86a8ed7031c0a595d539f862 100644 (file)
--- 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 ab4ad4c2d214986a7e772f2cce451e1043e14580..91748c17f64b0e6f72f5e00017500f585bdca1c7 100644 (file)
--- 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 efcfc9f21f811083093d0b0f4b87fa79bd2296b0..eb94e08e2ef0bfe1cb737ac03a0e0a6266b7b2e1 100644 (file)
--- 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 d02e348ee217a9378346ae839bc3ca52f04e2e42..69d89ee91f74c3c9bb2b42a97614447dae81472c 100644 (file)
--- 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 ca2631827a7ad0f9827aa618b7a1e55487c5a5b0..77abdbeea86449f98142fabe5baf9c93441f905f 100644 (file)
--- 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 bb79a3b0f8da1b8a930ce59a4f393a1305740c74..f04d0b10cd69dc232a4687af26f9bd2d96263e15 100644 (file)
--- 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 77f2537c6d9972211cbe8159ced236e88f983bb6..f9dbfb85ef4b2d9139c407510e68ddaeb6a5d41e 100644 (file)
--- 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 a2cc53bc73b335117400bb4a55fe95e138d29859..09e45674e91206425563b756fcb890184fe5c82d 100644 (file)
--- 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 d683744ff4d936d70bb0b508434cbe3851b4afea..e411b5724eb3e56c861d5ec0480b1e2a05eaefb1 100644 (file)
--- 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 e64a752dc207140f58781edbb4c90dfbacb05f8e..396c9dd37dc5f40bc4085d7c9ecf66d72eb0059c 100644 (file)
--- 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 6b5ac4a2aee863211dcc6773d972d1ff3d093399..0a2a60ff2d035c8b67cea160897435b7f680523f 100644 (file)
--- 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 467c25cac0f4aa44eb40900977aab6fdc03990ea..df8fe3ff816b141ef62d80800ae6b9ce6ed5b1ae 100644 (file)
--- 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 190874f56a91fd2c3b6bf61d6529aac040cacff3..5a76d9981c6c94125ed6f7f4c24d408f6836c882 100644 (file)
--- 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 dd2e955db5135a60778d56934a92fd37459aca21..b647dce22c5cf613e125ddf01de314fdc43fdc70 100644 (file)
--- 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 d914e6b246bf9382c073f93d56583e555d811ff5..cf0a795d9d0eea82edfbf468ea6c171638e9124a 100644 (file)
--- 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 cfddf667021aeda5e08bfe966cbebac4805068c6..16cd566aafe5d39204d07792670a95776d312bc7 100644 (file)
--- 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 e919cd310513416c711484e10bdf8a73de260025..118437264c9152daea23bf360c01f62780c6ab33 100644 (file)
--- 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 5d1418cbc6c42a3a31926db83a229876358413f0..9720c564a00617e339a5e2271326b47ddc3f1640 100644 (file)
--- 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 14f0155adb91029d0a72ac4807d84f4c115a85c8..f740a647f82b0525c3d4106bba2baf2e54bec7bc 100644 (file)
--- 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 53f1956a6ca641eb44ee52bc16d78276da1829bd..760a125648fcf34ea367236cffd39bf00e1867f4 100644 (file)
--- 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 bccea60944b91d60bf4e77735bd441f2533a72eb..1f6da909a86bf0e873704f4a8ec0ac500139a329 100644 (file)
--- 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 4cbe988a86c283eb9df5de45faf086e777ee2810..0f9ec0dbb788cffd3bdcc57cd2cabe647d63c89e 100644 (file)
--- 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 3bab0d3b1d524918359d1d631c2018c6e7be9c9c..4189216495b9f856caeb22b12257043a1e561846 100644 (file)
--- 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 1e4e99e7d25dd2034140e86462c1b62805ef154f..e44ea55db0a29ecb3e442f7b897c1bc5f759a690 100644 (file)
--- 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 b05d41157a99b3c20cfe202e43a069a0f858c87e..c37de12c23a4026677abd7d9b39c4f451db64845 100644 (file)
--- 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 a85c49cfe7065a0e5b366e6537ec54e92354a710..ccaa5e80ed9117015c7cfab17685338fbde67c13 100644 (file)
--- 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 3ece06e99aaedd42298f050e2417e946dba857e0..74691ad6d993db1c94400fa0e23b3da7bc55ff3f 100644 (file)
--- 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 134e7897fb0b0a62504b1ef0b6beabf7adac1c16..a82d60e8853d60b6d10547752a3807d1f87af845 100644 (file)
--- 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 24ddd7e3d70e4ef3005460e82e0da1ccedab3d48..e743542a3a2f5492fbc4ff6701852b9fb04d8a0f 100644 (file)
--- 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 f91a42464c0b3f58af381a6768e61b621ff79d37..5b2a189eca6ea48fcee3e08329aa125d17897cd9 100644 (file)
--- 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 f27de51d0923609bc7c7f9b18e9b468fee0ec280..66ef7c5558379639f65ac844bad7c4dec6d1c1a0 100644 (file)
--- 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 881af350af18a34c14ffa1256b72d810da1af9d0..c89d132522e546aa1db50261ca66db7fece65d28 100644 (file)
--- 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 8508efdc8ccaa0f3046f68e974feb621ab5941b5..0e9eac4745f98db0ab41fa1be27db298171c12d7 100644 (file)
--- 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 b30ce397a58c530390bbe9da1823b7fcbd143a68..354515802b3494f2f2836b55e56cc010999d0667 100644 (file)
--- 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 8d358e3512d4ff9af27f57aad471b47887b28af3..9def73c5ffc4122105796d648f8ae6cc0ea13766 100644 (file)
--- 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 03160a58c2d37d36ed9fcf4c877e4c9c70783c6d..dd33c8ed7934b70447283f1cdf99c655b3571f10 100644 (file)
--- 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 d0e3599f77f61391ad6bcab3d90ff5a4a43268c4..06dfd2c5e67657df196dda52ac94c0fcd9aa4120 100644 (file)
--- 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 9ccd994e9fd70586a38055e7d99ad63d0295a5c5..1305cf6ce697abbedd06b26ab36547c0c028676c 100644 (file)
--- 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 de36114c9930825bb4fc1d52021f6e67b7416d53..965637bc7f8e67e5afc257ae5ee4992a8c3cc3d3 100644 (file)
--- 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 4e19411a9b6703d544b5c6ce1ea68f974351e5e0..19b676eca5eb93297ab49e943195426d36d4e1ce 100644 (file)
--- 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 9d72d695cb0810188fa7e090bdfeaf96f3a1715d..3c25c6ffe16decf017a6fe3a14bf9eaf70f8d21e 100644 (file)
--- 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 4693754cded2113b70c1c6fbe41af14ffc361ef3..5b583615e33045c3e639f5d07344ef0137d80dec 100644 (file)
--- 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 7a6ff41192e997b9f7c1cc03a402f937a20d9819..e637e7d4ae1d4ff7861b9bb172602024417d8053 100644 (file)
--- 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 a317d5a15722864e21c1774036a5afd02595b8d8..6f271dd691935c2a4d4e0cf753a978f6ca380fd7 100644 (file)
--- 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 d64555fdc5c542e354bad8c2270193a90238b40a..77eef1f7348b6656130b56cda1704d5ca09e8ea0 100644 (file)
--- 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 61b2a80207f8f062093b6019b07a2f3ef28b75b4..c2656bf79a7bfbb19129c66e31d9d599d11d6feb 100644 (file)
--- 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 290d935a0da248505e70867b9c336ed74a3aa4d7..6bf34a8065f4b8bfb9089ac5472cde1d9f364f7f 100644 (file)
--- 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 d1a988c930cf03421516ffc989c831d8e87be498..15eeca8092690919c8f7358f2de7b7e586f2ddb5 100644 (file)
--- 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 e1cc77b66c8736c490aaba7ba35213216ce29845..ee30724b27669acce4d0eeed05f82fd08eef7806 100644 (file)
--- 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 c68f5a3bb1d5d3f1d220ef4b5854b76184af9594..413d5d0d0ae2111e71b2b4cd4e661cd9a3831f7f 100644 (file)
--- 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 e1f6f5844c41b305a634027b61f097930b11f8e2..c9075f2e3d960abb7cd093f1e51f1b9c047cd6c7 100644 (file)
--- 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 de8d7776002b135512788fa7a967e944e6aa8f2f..ba2e724eb7f4d59f21fc50ed45360a38dfa2de50 100644 (file)
--- 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 098aff3818b81912e4780b02188fe4679f3794a6..548df9d84689b87a07c2141a8b6aa95817c48219 100644 (file)
--- 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 d9727fe9002f0c248d790491e1c4680c66498369..570d2372434417a723d37f31646cbc0159160bc0 100644 (file)
--- 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 17b66a72f8f23168e8963913f22375395c0e4284..05e4b3cfdf3710308a0b8e99cc797af948a5abaf 100644 (file)
--- 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 b37752561279f8ca625406f22d73690638fcccf2..ea3be43e0cc565d3fdbca082377979461c2d09a8 100644 (file)
--- 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 6c05f2e05d6d811f5b384c1806c5b4ff785d83c3..e2a7df88456b79ca4a2f9b9199c5ac54f35981ff 100644 (file)
--- 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 d9a5f5c07874faaab886219d3f6ab8fccc2bcaa0..1bc6a7ee45f8a4a2288e57189932f4029c3c25b3 100644 (file)
--- 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 76e8e97aa370ad157d7452dcf1cf48d438eea240..8c38afbd9455d75efdef35a71c5719f252018ca2 100644 (file)
--- 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 67276324038aa31afdc651114009a45952849bab..766232ffd23b405013ec932446e4da0d0395203a 100644 (file)
--- 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 a92adbdd7d8c74eb67e86564d054bb5e79014b2d..f71b12e5795ebb3f6099d2d16c6db33ccb65e528 100644 (file)
--- 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 38a627df915a8540b5461cfb30f8f711a491c96e..919437549e3b8f26c108e2a1f1182f7b4ae5cbb7 100644 (file)
--- 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 07a4b2598db02a14abbddb69e5ac99fe17d287f1..e69046020a357bc7cbd52363dbd596776d10151d 100644 (file)
--- 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 56c0f69a404b0872cb9b5c04ac700d0a0deb31d6..4ed8eaa55416a09cb3200d6d62354ca4b5265e63 100644 (file)
--- 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 cd72ff7eea9c395b7f0d16a45c8868690a28eeac..4e85774004fa4d46f5decdb2fafc7b5908cdd45e 100644 (file)
--- 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 828dfc8ab233c2aebc59cf6131ce1655ffafe786..072bd65e8b4715ceca8176643ea1dc77d513b6c4 100644 (file)
--- 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 addf036aa255e55dce2f6500fe34497da6b189cd..cf69fbdd75cbb4e9186eb4a70b54fae0badfc764 100644 (file)
--- 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 47e7f8f0e170f000bed30ff4f1ae19e9fcbf2322..6d42028e093254c710cac425c7c1ef4cb2a9fc72 100644 (file)
--- 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 8e45dc567781dcbba0591322244a35ace2d9e18c..45c5189c7af88c3e0e7b232b8eda7e70d476d8f3 100644 (file)
--- 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 e09864dace5d2e7af543057c39684549cfaf6137..87a148225062a6a710b472ca5a62c189c076fc08 100644 (file)
--- 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 6a7895e1ccb6b83f3e69afea5516bf863ddf1c3e..c4c03e265cfe993bb444377ae746c4dd0a05ece6 100644 (file)
--- 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 9cc37832aaad75dd8542ed5e826ed38eabf1ff34..bf43acb8306c26d9bed162251fe2549ba9d67f1f 100644 (file)
--- 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 a71e1278803b44f99d9b94ea2abbcc759b10d7fe..83f8399f9e4ebd11090c75600fa59bda4bae3785 100644 (file)
--- 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 04ec616b7e3058f597ff0ce275c6f9ccff9f8b48..d4cd09aedd1d6623209cf006bb4c8c149cb77e51 100644 (file)
--- 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 445fca829956b61fba383982cc3648991f14a06d..22f1826a9d5840d1524007eb791c436ffa2f565d 100644 (file)
--- 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 7504ce588ce440bd6a432bf6066da15ec81b07af..6e86e46db308d02a906c4747714c49190dfd6c1b 100644 (file)
--- 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 38d3ab4c5b542855be99c23121cae7726327793a..1b7c4e2853345c3b93d0f884b6a468b45f0e55b8 100644 (file)
--- 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 d75a6d96e07fe0c4e77d25115134c64a9e003ec4..e5c9a4810d8cdf817c3d24db7f2af6772bafd2c1 100644 (file)
--- 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 ea2608643a7ccabf18c454ba2a805830708dc4f8..c82d5ad140c26c731b5c818f426380a90dcbda6c 100644 (file)
--- 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 644471972ee01373a21cb39e865b642618d1141a..a5656dbb8268212c2e8da2abeac629c3aefec831 100644 (file)
--- 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 f3f5e7595068c182fda08a1576a42bc66e23b59d..90502489c992720d46b8bc903179f52ab4f2ba60 100644 (file)
--- 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 3d08d1bcd5a4e6881167c7441b9a754c96a0cf49..249f09a22f8b6cc53c815acc3b1d5665457801b6 100644 (file)
--- 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 d3f15e917b77473f93aa88cd200c0ce0b6291cf0..e14e0768e5da91d26cd0bf32f8363939bf6b90da 100644 (file)
--- 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 e5f87cd2122f58c46d07a29bc0147881396eb3a7..2cc1a75360b5c182f2c567f775118f45099e403b 100644 (file)
--- 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 806f1bdc4b43d9443cde16616afc215e94d5620b..6a77615a3f3aa20a1755a7a1ddaac2abad5ea516 100644 (file)
--- 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 4b535916ee3c86b53548f66933cefb2dc6570a23..7b76445f470f83a5ab69426563d1324ccc2101ad 100644 (file)
--- 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 26ad559034fff1f0a33317eb68f04881a5bc5128..9373a9beda203bd0b5c9ad864c524cf7c7b361b5 100644 (file)
--- 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 58208932bf9b6a2ac8b078fc64514f3f15e485a8..d4571bf7f58cd9ddba8bbb5efdda4d8c4a6a62bb 100644 (file)
--- 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 95c6389c95e17cb4e28e5fcd63c791d7f8ac45a5..34f8df65a12ab118c387996bf192f86b694aa89a 100644 (file)
--- 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 6817807315ddda3508ffc740044623a8cd50c6df..e8091c2ab9e09065968fd48e0be5a097d15ed71b 100644 (file)
--- 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 4dc584bd3582bfb39058b6629f784666a01acece..6fac0285c98f783de5338283a6a14e5ff0f36be4 100644 (file)
--- 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 46a932900bc013707bb404470e76768095f066c1..0fcc15b76486d65898593527e56bea675c6c21b0 100644 (file)
--- 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.