let rec solve e =
  solvel ([e], [])

and solvel (el, sl) =
  match el with
    | [] -> sl
    | (a, b) :: el1 ->
        solve1 (a, b) (el1, sl)

and solve1 (a, b) (el, sl) = 
  if Term.eq a b then                              (* [Triv] *)
    solvel (el, sl)
  else 
    match destruct a, destruct b with
      | Some(Sym.In(x), a'), Some(Sym.In(y), b') -> 
          if x = y then                            (* [Inj=] *)
            solvel ((a', b') :: el, sl)          
          else                                     (* [Inj/=] *)
            raise Exc.Inconsistent              
      | Some(Sym.In(x), a'), Some _ ->             (* [Slv] left *)
          solvel ((a', mk_outX x b) :: el, sl)
      | Some _, Some(Sym.In(x), b') ->             (* [Slv] right *)
          solvel ((b', mk_outX x a) :: el, sl)
      | Some(Sym.Out(x), a'), Some(Sym.Out(y), b') -> 
          if x = y then                            (* [Out=] *)
            solvel ((a', b') :: el, sl)           
          else                                     (* [Out/=] *) 
            solvel ((a', mk_inX x b) :: el, sl)
      | None, Some _ -> 
          if occurs a b then                       (* Bot *) 
            raise Exc.Inconsistent
          else 
            solvel (install (a, b) (el, sl))
      | Some _, None -> 
          if occurs b a then                       (* Bot *) 
            raise Exc.Inconsistent
          else 
            solvel (install (b, a) (el, sl))
      | None, None -> 
          solvel (install (Term.orient (a, b)) (el, sl))

and install (x, b) (el, sl) =
  assert(not(occurs x b));
  let el' = substitute (x, b) el                  (* Subst *)
  and sl' = Term.Subst.compose apply (x, b) sl in
    (el', sl')

and occurs x a =
  assert(not(is_interp x));
  try
    let (_, b) = d_interp a in
      occurs x b
  with
      Not_found -> Term.eq x a

and substitute (x, b) el =
  let apply2 (a1, a2) =
    (apply (x, b) a1, apply (x, b) a2)
  in
    List.map apply2 el