Branched paramodulation for CNF (Horn clauses)

[helm.git] / helm / software / components / tptp_grafite / parser.mly

diff --git a/helm/software/components/tptp_grafite/parser.mly b/helm/software/components/tptp_grafite/parser.mly
index 4fe172144a4a2636f11f0d840c42ed07fc9f0624..0f3525689212de5c2ae37b3a20d91363018f3afd 100644 (file)
--- a/helm/software/components/tptp_grafite/parser.mly
+++ b/helm/software/components/tptp_grafite/parser.mly
@@ -56,7 +56,12 @@
             name COMMA formula_type COMMA formula formula_source_and_infos 
           RPAREN DOT {
             AnnotatedFormula ($3,$5,$7,fst $8,snd $8)  
-      }
+         }
+    | CNF LPAREN
+         TYPE COMMA formula_type COMMA formula formula_source_and_infos
+       RPAREN DOT {
+         AnnotatedFormula ($3,$5,$7,fst $8,snd $8)  
+       }
   ;
   
   formula_type: