made executable again

[helm.git] / helm / software / matita / contribs / ng_TPTP / COL058-3.ma

diff --git a/helm/software/matita/contribs/ng_TPTP/COL058-3.ma b/helm/software/matita/contribs/ng_TPTP/COL058-3.ma
index dff033e64ef7137c9460e8ed7bdbd715a5f45816..4a51f4ff503e829e81c8b82dec0ddc5b3a6c7710 100644 (file)
--- a/helm/software/matita/contribs/ng_TPTP/COL058-3.ma
+++ b/helm/software/matita/contribs/ng_TPTP/COL058-3.ma
@@ -4,7 +4,7 @@ include "logic/equality.ma".
 
 (* -------------------------------------------------------------------------- *)
 
-(*  File     : COL058-3 : TPTP v3.2.0. Released v1.0.0. *)
+(*  File     : COL058-3 : TPTP v3.7.0. Released v1.0.0. *)
 
 (*  Domain   : Combinatory Logic *)
 
@@ -56,18 +56,19 @@ include "logic/equality.ma".
 
 (* ---- Hypothesis: This bird is egocentric  *)
 ntheorem prove_the_bird_exists:
- ∀Univ:Type.∀X1:Univ.∀X2:Univ.
+ (∀Univ:Type.∀X1:Univ.∀X2:Univ.
 ∀lark:Univ.
 ∀response:∀_:Univ.∀_:Univ.Univ.
-∀H0:∀X1:Univ.∀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)))
+∀H0:∀X1:Univ.∀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))))
 .
-#Univ.
-#X1.
-#X2.
-#lark.
-#response.
-#H0.
-nauto by H0;
+#Univ ##.
+#X1 ##.
+#X2 ##.
+#lark ##.
+#response ##.
+#H0 ##.
+nauto by H0 ##;
+ntry (nassumption) ##;
 nqed.
 
 (* -------------------------------------------------------------------------- *)