let rec is_connected =
  let module Hash = Hashtbl.Make(
      struct
        type t = (atom * int) * (atom * int)
        let equal (a1, a2) (b1, b2) = equal a1 b1 && equal a2 b2
        let hash ((_, n), (_, m)) = (n + m) land 0x3FFFFFFF
      end)
    in
    let table = Hash.create 17 in
    let _ =  Tools.add_at_reset (fun () -> Hash.clear table) in 
      fun atm1 atm2 ->
        try
          Hash.find table (atm1, atm2)
        with
            Not_found ->
              let result = is_connected0 atm1 atm2 in
                Hash.add table (atm1, atm2) result; 
                result
   
and is_connected0 (atm1, _) (atm2, _) =  
  let rec term_is_connected = function
    | Term.Var _ as x -> occurs (x, atm2)
    | Term.App(_, sl, _) -> List.exists term_is_connected sl
  in
    match atm1 with
      | TT -> false
      | FF -> false
      | Equal(a, b) -> term_is_connected a || term_is_connected b
      | Diseq(a, b) -> term_is_connected a || term_is_connected b
      | Nonneg(a) -> term_is_connected a
      | Pos(a) -> term_is_connected a