From c43c06062d86bb62bd259537f18aa587699aad9c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 19 May 2009 14:34:01 +0000 Subject: [PATCH] NotEq is now considered as a negative Eq atom --- helm/software/components/tptp_grafite/tptp2grafite.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index 7a714ce07..6b98fe515 100644 --- 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 ;; -- 2.39.2