NotEq is now considered as a negative Eq atom

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index 7a714ce0704ee8843ad64d172fd2c6bc962ecd9d..6b98fe51570291c84fdaf7a2305f9b70da1d7bdf 100644 (file)
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -89,6 +89,7 @@ let rec atom_of_formula neg pos = function
         let neg, pos = atom_of_formula neg pos a in
         atom_of_formula neg pos b 
     | A.NegAtom a -> a::neg, pos 
+    | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
     | A.Atom a -> neg, a::pos
 ;;