let simplify ~(print:bool) ~(equality:bool) (clauses: clause list) : clause list * literal list =
  if print then begin
    print_endline ("Preprocessing: Pure Literals");
  end;

  (* for equality we can not go by unification,
     or perhaps somewhat if we take sorts (Sort_inference) into account.
     currently pure is detected by predicate symbol polarity only.
  *)
  if equality then begin
    (* keep from each predicate symbol a mapping index -> contained in claused *)
    let index =
      Term.LiteralTypeTable.create 1024
    in

    (* now register all clauses *)
    List.iter
      (fun clause ->
        List.iter
          (fun literal ->
            let entry =
              try
                Term.LiteralTypeTable.find index literal
              with
                | Not_found ->
                    let new_entry =
                      ref []
                    in
                      Term.LiteralTypeTable.add index literal new_entry;
                      new_entry
            in
              entry := clause :: !entry;
          ) 
          clause
      )
      clauses;

    (* all unifiable literals must be from the clause itself *)
    let is_pure (clause: clause) (literal: literal) : bool =
      let matching =
        Term.LiteralTypeTable.find index (Term.request_negated_literal literal)
      in
        List.for_all
          (fun clause' -> clause == clause')
          !matching
    in

    (* now check for each clause if one of its literals is pure,
       i.e. its negation is not unifiable with a literal from another clause. *)
    let purified, pure_literals =
      purify ~print:print ~fix:true is_pure clauses
    in
      if print then begin
        print_newline ();
      end;
      purified, pure_literals
  end

  (* purity check via unifying literals *)
  else begin
    (* keep from each literal a mapping index -> contained in claused *)
    let index =
      Discrimination_tree.create_clause_index false
    in

    (* now register all clauses *)
    List.iter
      (fun clause ->
        List.iter
          (fun literal ->
            (index#find literal)#add literal.Term.atom clause
          ) 
          clause
        )
      clauses;

    (* all unifiable literals must be from the clause itself *)
    let is_pure (clause: clause) (literal: literal) : bool =
      let unifiable =
        (index#find (Term.request_negated_literal ~insert_db:false literal))#find_all_unifiable
          ~p_preserving:false literal.Term.atom
      in
        List.for_all
          (fun clause' -> clause == clause')
          unifiable
    in

    (* now check for each clause if one of its literals is pure,
       i.e. its negation is not unifiable with a literal from another clause. *)
    let purified, pure_literals =
      purify ~print:print ~fix:false is_pure clauses
    in
      if print then begin
        print_newline ();
      end;
      purified, pure_literals
  end