X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_TPTP%2FBOO006-4.ma;h=000c97620414b5c10b7d5d6d131906083d1fda40;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=e2647ce1f5761d25bd3a7b64faf6d084d7b7e80d;hpb=0639dda9142d1cf047b07e61fb557e8877aba4d8;p=helm.git diff --git a/helm/software/matita/contribs/ng_TPTP/BOO006-4.ma b/helm/software/matita/contribs/ng_TPTP/BOO006-4.ma index e2647ce1f..000c97620 100644 --- a/helm/software/matita/contribs/ng_TPTP/BOO006-4.ma +++ b/helm/software/matita/contribs/ng_TPTP/BOO006-4.ma @@ -4,7 +4,7 @@ include "logic/equality.ma". (* -------------------------------------------------------------------------- *) -(* File : BOO006-4 : TPTP v3.2.0. Released v1.1.0. *) +(* File : BOO006-4 : TPTP v3.7.0. Released v1.1.0. *) (* Domain : Boolean Algebra *) @@ -48,7 +48,7 @@ include "logic/equality.ma". (* -------------------------------------------------------------------------- *) -(* File : BOO004-0 : TPTP v3.2.0. Released v1.0.0. *) +(* File : BOO004-0 : TPTP v3.7.0. Released v1.0.0. *) (* Domain : Boolean Algebra *) @@ -68,7 +68,7 @@ include "logic/equality.ma". (* Syntax : Number of clauses : 8 ( 0 non-Horn; 8 unit; 0 RR) *) -(* Number of literals : 8 ( 8 equality) *) +(* Number of atoms : 8 ( 8 equality) *) (* Maximal clause size : 1 ( 1 average) *) @@ -123,6 +123,7 @@ ntheorem prove_right_identity: #H6 ##. #H7 ##. nauto by H0,H1,H2,H3,H4,H5,H6,H7 ##; +ntry (nassumption) ##; nqed. (* -------------------------------------------------------------------------- *)