let compute_resolvents ~(print:bool) (clauses: clause list) : clause list =
  if print then begin
    print_endline ("Preprocessing: Computing resolvents of size <= " ^ string_of_int Const.resolvent_max_size);
  end;

  (* register all literals of clauses with length <= max_size + 1 -
     to speed up computation we ignore the others right away. *)
  let index =
    Discrimination_tree.create_index false (new data)
  in
    List.iter
      (fun clause ->
        let length =
          List.length clause
        in
          if length <= Const.resolvent_max_size + 1 then begin
            List.iter
              (fun literal ->
                (index#find literal)#add literal.Term.atom (literal, clause, length)
            ) 
            clause
          end;
      )
      clauses;
  
  (* compute resolvents for each clause *)
  let resolvents, _ =
    List.fold_left
      (fun (resolvents, number_of_resolvents) clause ->
        if number_of_resolvents >= Const.resolvents_max_number then
          (resolvents, number_of_resolvents)

        else if List.length clause <= Const.resolvent_max_size + 1 then
          compute_resolvents_for_clause ~print:print
            index resolvents number_of_resolvents clause

        else
          (resolvents, number_of_resolvents)
      )
      ([], 0)
      clauses
  in

  (* drop resolvent if it already exists as a clause *)
  let resolvents =
    List.find_all
      (fun resolvent ->
        List.for_all
          (fun clause -> not (Term.clause_equal resolvent clause))
          clauses
      )
      resolvents
  in

  (* keep only the shortest resolvent *)
  let resolvents =
    Tools.list_first Const.resolvents_max_number
      (
        List.sort
          (fun x y ->
            let length =
              Tools.compare_int (List.length x) (List.length y)
            in
              if length != 0 then
                length
              else
                Tools.compare_int (Term_attributes.weight_of_clause x) (Term_attributes.weight_of_clause y)
          )
          resolvents
      )
  in

    (* resolve resolvents *)
  let resolvents', _ =
    List.fold_left
      (fun (resolvents, number_of_resolvents) clause ->
        if number_of_resolvents >= Const.resolvents_max_number then
          (resolvents, number_of_resolvents)

        else if List.length clause <= Const.resolvent_max_size + 1 then
          compute_resolvents_for_clause ~print:print
            index resolvents number_of_resolvents clause

        else
          (resolvents, number_of_resolvents)
      )
      ([], 0)
      resolvents
  in
  let resolvents' =
    List.find_all
      (fun resolvent ->
        List.for_all
          (fun clause -> not (Term.clause_equal resolvent clause))
          clauses
      )
      resolvents'
  in
  let resolvents' =
    List.find_all
      (fun resolvent ->
        List.for_all
          (fun clause -> not (Term.clause_equal resolvent clause))
          resolvents
      )
      resolvents'
  in
  let resolvents =
    Tools.list_first Const.resolvents_max_number
      (
        List.sort
          (fun x y ->
            let length =
              Tools.compare_int (List.length x) (List.length y)
            in
              if length != 0 then
                length
              else
                Tools.compare_int (Term_attributes.weight_of_clause x) (Term_attributes.weight_of_clause y)
          )
          resolvents' @ resolvents
      )
  in

    if print then begin
      print_newline ();
    end;
    resolvents