X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_TPTP%2FCOL063-5.ma;h=5edd4ccc467a5059e108b979751b36031856b372;hb=02e8b3eb9d2a8a3bb3942c41b47b6ac048efd5be;hp=a49f38c46f956d6a0bed4dc3126a8556e546bfd5;hpb=0639dda9142d1cf047b07e61fb557e8877aba4d8;p=helm.git diff --git a/helm/software/matita/contribs/ng_TPTP/COL063-5.ma b/helm/software/matita/contribs/ng_TPTP/COL063-5.ma index a49f38c46..5edd4ccc4 100644 --- a/helm/software/matita/contribs/ng_TPTP/COL063-5.ma +++ b/helm/software/matita/contribs/ng_TPTP/COL063-5.ma @@ -4,7 +4,7 @@ include "logic/equality.ma". (* -------------------------------------------------------------------------- *) -(* File : COL063-5 : TPTP v3.2.0. Bugfixed v1.2.0. *) +(* File : COL063-5 : TPTP v3.7.0. Bugfixed v1.2.0. *) (* Domain : Combinatory Logic *) @@ -30,7 +30,7 @@ include "logic/equality.ma". (* Status : Unsatisfiable *) -(* Rating : 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.43 v2.0.0 *) +(* Rating : 0.11 v3.4.0, 0.12 v3.3.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.43 v2.0.0 *) (* Syntax : Number of clauses : 3 ( 0 non-Horn; 3 unit; 1 RR) *) @@ -77,6 +77,7 @@ ntheorem prove_f_combinator: #H0 ##. #H1 ##. nauto by H0,H1 ##; +ntry (nassumption) ##; nqed. (* -------------------------------------------------------------------------- *)