let condense (clause: clause) : clause =

  let rec condense' (condensed: clause) (to_process: literal list) : clause =
    match to_process with
      | [] ->
          (* all clause literals checked, so this is the condensed literal *)
          condensed

      | head :: tail ->
          print_endline (Term.literal_to_string head);
          (* a ground literal must be part of the condensed clause -
             assuming no literal exists more than once in a clause. *)
          if Term.is_term_ground head.Term.atom then begin
            condense' condensed tail
          end
            
          (* cheack precheck:
             head must be more general than another clause literal. *)
          else if
            List.for_all
              (fun x ->
                 (Term.literal_equal head x)
                 ||
                 begin
                   try
                     ignore (match_literals ~recompute:false head 0 x 1 : subst);
                     false
                   with
                     | UNIFICATION_FAIL  ->
                         true
                 end
              )
              condensed
          then begin
            condense' condensed tail
          end


          else begin
            (* the potentially condensed clause *)
            let condensed' =
              Tools.list_remove_first
                (Term.literal_equal head)
                condensed
            in
              if subsumes condensed condensed' then
                (* yes, condensed *)
                condense' condensed' tail
              else
                (* no, keep previous clause *)
                condense' condensed tail
          end
  in
  (*condense' clause clause*)
  let ground, non_ground =
    List.partition Term.is_literal_ground clause
  in
  let condensed =
    condense' non_ground non_ground
  in
    ground @ condensed