let rec is_true (context: context) (literal: literal) : bool =
  (* contradictory? *)
  match check_contradictory context literal with
    | Some _ ->
        false

    | None ->
        (* p-instance of a context literal? *)
        begin
          match check_subsumed context literal with
            | Some _ -> true

            | None ->
                (* produced? *)
                let generalizations =
                  (context.index#find literal)#find_all_generalizations
                    ~p_preserving:false literal.Term.atom
                in
                  List.exists
                    (fun generalization ->
                      match check_productive context
                        generalization.el_literal
                        (Term.request_negated_literal ~insert_db:false literal)
                      with
                        | None ->
                            (* a positive produced literal is true in the interpretation,
                               but for a negative one we have to check that the positive one
                               is not produced as well. *)
                            if literal.Term.sign then
                              true
                            else
                              not (is_true context (Term.request_negated_literal ~insert_db:false literal))
                        | Some _ -> false
                    )
                    generalizations
        end