let rec diseq d s =  
  Trace.msg "p" "Diseq" d Fact.pp_diseq;
  let (x, y, _) = Fact.d_diseq d in
    match is_equal s x y with
      | Three.Yes -> 
          raise Exc.Inconsistent
      | Three.No -> 
          (nochange, s)
      | Three.X -> 
          let (chd', d') = D.add d s.d in
          let (chc', c') = C.diseq d s.c in
          let ch' = {nochange with chd = chd'; chc = chc'} in
          let s' = update_c (update_d s d') c' in
            (ch', s')