let add_lemma lemmas_propositional clause global =
  (* first normalize all variables, independent of each other.
     this is the clause used for variant elimination *)
  let clause' = 
    Term.sort_clause (
    List.map
      (fun literal -> Subst.apply_to_literal Subst.empty literal 0)
      clause
    )
  in

  if filter_lemma lemmas_propositional clause' then begin
    ()

  end
  else begin
  prune_lemmas lemmas_propositional;

  (* now skolemize clause, this is the claus used for propagation *)
  let clause =
    Term.request_skolemized_clause clause'
  in
  (* find abstraction of clause and remove variants.
     E.g. p(x) \/ p(y) becomes p(x) *)
  let abstraction =
    List.fold_left
      (fun acc literal ->
         let literal =
           Subst.apply_to_literal Subst.empty literal 0
         in
         try
           let abstraction =
             LiteralTable.find lemmas_propositional.literal_to_abstraction literal
           in
             Tools.list_add (==) acc abstraction
         with
           | Not_found ->
               (* can only be false or undetermined *)
               let status =
                 match Context.check_contradictory lemmas_propositional.context literal with
                   | None ->
                       Undetermined
                   | Some element ->
                       False element
               in
               let abstraction = {
                 abs_literal = literal;
                 abs_status = status;
               }
               in
                       LiteralTable.add lemmas_propositional.literal_to_abstraction literal abstraction;
                 (lemmas_propositional.subsumed#find literal)#add literal.Term.atom abstraction;
                 abstraction :: acc
      )
      []
      clause
  in
  let abstraction =
    Array.of_list (List.rev abstraction)
  in

  (* ignore duplicates *)

  (* create the context_unifier_space of this lemma -
     just to later on propagate a candidate to the assert candidat set. *)
  let input_partners =
    Array.mapi
      (fun i abstraction ->
         Context_unifier.create_input_partner
           i
           abstraction.abs_literal
           []
      )
      abstraction
  in
  let space =
    Context_unifier.create_space
      (Context_unifier_space.get_id lemmas_propositional.space_registry)
      clause
      [] (* considered to be ground *)
      []
      []
      input_partners
      [| |] (* no ordering ever needed *)
      lemmas_propositional.process_close
      lemmas_propositional.process_assert
      (fun _ -> ()) (* no split candidates computed *)
      (fun _ -> false) (* not used in recomputation of candidates *)
      (fun _ -> false) (* not used in recomputation of candidates *)
      true          (* this is a lemma *)
  in

  let lemma = {
    clause = clause;
    space = space;
    global = global;
    abstraction = abstraction;
    watched1 = 0;
    watched2 = (-1);
  }
  in

  (* register watched literals *)

    if Array.length abstraction > 1 then begin
      lemma.watched1 <- find_watched_literal abstraction 0 (-1);
      lemma.watched2 <- find_watched_literal abstraction (lemma.watched1 + 1) lemma.watched1;

      if lemma.watched1 == Array.length abstraction then begin
        failwith "new lemma: all literals falsified"
      end;

      (* for bad lemmas this need not to happen,
         as one literal is instantiated to several. *)
      if lemma.watched2 = Array.length abstraction then begin
        if lemma.watched1 = 0 then
          lemma.watched2 <- 1
        else
          lemma.watched2 <- 0;

        register_watched_literal lemmas_propositional lemma.abstraction.(lemma.watched1) lemma;
        register_watched_literal lemmas_propositional lemma.abstraction.(lemma.watched2) lemma;

        (* check if this lemma creates a unit propagation *)
        compute_propagation lemmas_propositional lemma;
      end

      else begin
        register_watched_literal lemmas_propositional lemma.abstraction.(lemma.watched1) lemma;
        register_watched_literal lemmas_propositional lemma.abstraction.(lemma.watched2) lemma;
      end;

    end

    else begin
      lemma.watched2 <- 0;
      register_watched_literal lemmas_propositional lemma.abstraction.(lemma.watched1) lemma;
      compute_propagation lemmas_propositional lemma;
    end;


    (* register lemma *)
    ClauseTable.add lemmas_propositional.lemmas clause' lemma;


    ()
  end