let split ~(print: bool) (clauses: clause list) : clause list =
  if print then begin
    print_endline ("Preprocessing: Ground Splitting");
  end;

  let labels =
    Labels.create 64
  in
  let connection_clauses =
    ConnectionClauses.create 64
  in
  let counter =
    Counter.create_with 0
  in

  (* split each clause *)
  let rec split' to_split already_split split_done =
    match to_split with
      | [] ->
          if print then begin
            print_endline ("Performed " ^ string_of_int (Counter.value counter) ^ " ground splits.");
            print_newline ();
          end;

          (* split done, so reverse the new clauses to get the original clause order *)
          if split_done then
            List.rev already_split

          (* no split done *)
          else
            clauses

      | clause :: tail ->
          begin
            match split_clause labels counter connection_clauses clause with
              | None ->
                  split' tail (clause :: already_split) split_done

              | Some split ->
                  if print then begin
                    print_endline ("Ground split: " ^ Term.clause_to_string clause);
                    List.iter
                      (fun clause ->
                         print_endline ("-> " ^ Term.clause_to_string clause)
                      )
                      split;
                    print_newline ();
                  end;                  

                  split' tail (split @ already_split) true
          end
  in
    split' clauses [] false