update in groud_2 and models

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

diff --git a/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma
index 86a05a99bf51b3a31016e2d727684e54a17f21c8..b109ddc682c0d15b9cf7b9377158312d4d9a0fba 100644 (file)
--- a/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/TPTP/COL058-2".
+
 include "logic/equality.ma".
 (* Inclusion of: COL058-2.p *)
 (* -------------------------------------------------------------------------- *)
@@ -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=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.