let solve i (a, b) = 
  try
    let e = Fact.mk_equal a b None in
      List.map (fun e' -> 
                  let (x, b, _) = Fact.d_equal e' in
                    (x, b))
        (Th.solve i e)
  with
    | Exc.Inconsistent -> raise(Invalid_argument("Unsat"))