A few more theorems.

[helm.git] / helm / software / matita / tests / TPTP / Veloci / COL058-3.p.ma

diff --git a/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma
index e36faea3324c1dc8e9d7660221f199cab7555127..2235cb57dae2bb5718682d40a44d6f19b8f4c2c3 100644 (file)
--- a/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma
+++ b/helm/software/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.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.