X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Ftests%2FTPTP%2FVeloci%2FCOL058-3.p.ma;h=f3e5b5d5221f91b2e1178c60fd33c7abb23cdbd2;hb=3dc6e3197a630bfd5fcd608fef3434c5448c94a1;hp=e36faea3324c1dc8e9d7660221f199cab7555127;hpb=fc8c0a2718023695bd5795a72af2d90ea8fe9243;p=helm.git

diff --git a/matita/tests/TPTP/Veloci/COL058-3.p.ma b/matita/tests/TPTP/Veloci/COL058-3.p.ma
index e36faea33..f3e5b5d52 100644
--- a/matita/tests/TPTP/Veloci/COL058-3.p.ma
+++ b/matita/tests/TPTP/Veloci/COL058-3.p.ma
@@ -35,7 +35,7 @@ theorem prove_the_bird_exists:
 \forall H0:\forall X1:Univ.\forall X2:Univ.eq Univ (response (response lark X1) X2) (response X1 (response X2 X2)).eq Univ (response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))
 .
 intros.
-auto paramodulation timeout=600.
+auto paramodulation timeout=100.
 try assumption.
 print proofterm.
 qed.