X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Ftests%2FTPTP%2FVeloci%2FGRP600-1.p.ma;h=965637bc7f8e67e5afc257ae5ee4992a8c3cc3d3;hb=fbdd1cc46819d19ed135391a4a954c19d1b92c0c;hp=de36114c9930825bb4fc1d52021f6e67b7416d53;hpb=fc8c0a2718023695bd5795a72af2d90ea8fe9243;p=helm.git

diff --git a/matita/tests/TPTP/Veloci/GRP600-1.p.ma b/matita/tests/TPTP/Veloci/GRP600-1.p.ma
index de36114c9..965637bc7 100644
--- a/matita/tests/TPTP/Veloci/GRP600-1.p.ma
+++ b/matita/tests/TPTP/Veloci/GRP600-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A B) (inverse (double_divide A (inverse (double_divide (inverse C) B))))) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-auto paramodulation timeout=600.
+auto paramodulation timeout=100.
 try assumption.
 print proofterm.
 qed.