let rec solve e =
  let (a, b, _) = Fact.d_equal e in
  let sl = solvel ([(a, b)], []) in
    List.map (fun (x, b) -> Fact.mk_equal x b None) sl
  
and solvel (el,sl) =
  match el with
    | [] -> sl
    | (a, b) :: el when Term.eq a b ->
        solvel (el,sl)
    | (a, b) :: el ->
        (match d_interp a, d_interp b  with   
           | None, Some _ when not(occurs a b) ->      (* Check if solved. *)
               solvel (add a b (el,sl))
           | Some _, None  when not(occurs b a) ->
               solvel (add b a (el,sl))
           | Some(Conc _, _), _                  (* Decomposition of conc. *)
           | _, Some(Conc _, _) ->
               solvel (decompose (a,b) @ el, sl)
           | Some(Bitwise(n), _), _ ->            (* Solve bitwise ops. *)
               solvel (solve_bitwise n (a,b) @ el, sl)
           | (None | Some(Const _, _)), Some(Bitwise(m), _) ->
               solvel (solve_bitwise m (a,b) @ el, sl)
           | Some(Const(c), []), Some(Const(d), []) ->
               if Pervasives.compare c d = 0 then 
                 solvel (el,sl)
               else 
                 raise Exc.Inconsistent
           | Some(Sub(n,i,j),[x]), Some(Sub(m,k,l),[y]) when Term.eq x y ->
               assert(n = m);
               let (x,b) = solve_sub_sub x n i j k l in
               solvel (add x b (el,sl))
           | Some(Sub(n,i,j),[x]), _ ->
               assert(n-j-1 >= 0);
               assert(i >= 0);
               let b' = mk_conc3 i (j-i+1) (n-j-1) 
                          (mk_fresh i) b (mk_fresh (n-j-1)) in
               solvel (add x b' (el,sl))
           | _, Some(Sub(n,i,j), [x]) -> 
               assert(n-j-1 >= 0); 
               assert(i >= 0);
               let b' = mk_conc3 i (j-i+1) (n-j-1) (mk_fresh i) 
                          b (mk_fresh (n-j-1)) in
               solvel (add x b' (el,sl))
           | _ ->
               let a, b = Term.orient(a,b) in
               solvel (add a b (el,sl)))

and solve_sub_sub x n i j k l =
  assert (n >= 0 && i < k && j-i = l-k);
  let lhs = 
    mk_sub n i l x 
  in
  let rhs =
    if (l-i+1) mod (k-i) = 0 then
      let a = mk_fresh (k-i) in
      mk_iterate (k-i) a ((l-i+1)/(k-i))
    else
      let h = (l-i+1) mod (k-i) in
      let h' = k-i-h in
      let a = mk_fresh h in
      let b = mk_fresh h' in
      let nc = (l-i-h+1)/(k-i) in
      let c = mk_iterate (h + h') (mk_conc h' h b a) nc in
      mk_conc h (nc * (h' + h)) a c
  in
  (lhs, rhs)