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 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) ^ " non-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
            let clause' =
              List.map
                (fun literal ->
                   literal, Term.vars_of_literal literal
                )
                clause
            in
              match split_clause labels counter clause' with
                | None ->
                    split' tail (clause :: already_split) split_done

                | Some [] ->
                    failwith "Preprocessing_split_ground.split: empty clause"

                | Some split ->
                    if print then begin
                      print_endline ("Non-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