let rec diseq d s =
  changed := Term.Set.empty;
  let s' = diseq1 d s in
    (!changed, s')

and diseq1 d s =
  let (x, y, prf) = Fact.d_diseq d in
    try
      let (i, prf1) = apply s x 
      and (j, prf2) = apply s y in
        if i = Sign.Zero && j = Sign.Zero then
          raise Exc.Inconsistent
        else 
          s
    with
        Not_found -> s