let print_tptp_model (context: context) (out: out_channel) (problem: problem)
    (finite_domain: finite_domain option) (bound: bound) : unit =

  begin
    match finite_domain with
      | Some _ -> tptp_print_finite_domain out bound;
      | None -> ()
  end;

  (* get the dig *)
  let dig : (symbol * ig list) list =
    tptp_get_dig context problem finite_domain
  in

  (* create the definition for each predicate *)
  let predicate_definitions : predicate_definition list =
    create_predicate_definitions dig
  in

  (* add predicates of which all instances are false *)
  let predicate_definitions =
    List.fold_left
      (fun acc symbol ->
        if not (Symbol.is_input symbol) then
          acc
            
        (* already defined? *)
        else if
          List.exists
            (fun definition ->
              Symbol.equal symbol (Term.top_symbol_term definition.pd_schema)
            )
            predicate_definitions
        then
          acc

        (* define all instances as false *)
        else begin
          let definition = {
            pd_schema = Term.create_schema_term symbol;
            pd_igs = [];
            pd_false = true;
          }
          in
            definition :: acc
        end
      )
      predicate_definitions
      problem#getPredicateSymbols
  in
  let predicate_definitions =
    List.sort
      (fun x y ->
        Symbol.compare_name
          (Term.top_symbol_term x.pd_schema)
          (Term.top_symbol_term y.pd_schema)
      )
      predicate_definitions
  in

  (* filter equality in finite domain mode *)
  let predicate_definitions =
    if finite_domain != None then
      List.find_all
        (fun definition ->
          not (Symbol.equal Symbol.equality (Term.top_symbol_term definition.pd_schema))
        )
        predicate_definitions
    else
      predicate_definitions
  in

  (* print the definitions *)
  begin
    match finite_domain with
      | None ->
          tptp_print_definitions predicate_definitions
            "interpretation, i_predicates"
            (*"*)
            out;

      | Some _ ->
          let function_definitions =
            create_function_definitions dig
          in

          (* first functions *)
          if List.length function_definitions > 0 then
            tptp_print_definitions function_definitions
              "interpretation_terms, fi_functors" out;
              (*" out;*)

          Print.output_line out "";
          
          (* then predicates *)
          if List.length predicate_definitions > 0 then begin
            tptp_print_definitions predicate_definitions
              "interpretation_atoms, fi_predicates" out;
              (*" out;*)
          end

          (* input better contains no predicates ... *)
          else begin
              (* there is a tptp problem (SYN916-1) which contains only true.
                 so the check below would crash in that case,
                 although everything is fine. *)
              (*
            if problem#containsEquality && List.length problem#getPredicateSymbols = 0 then
              Print.output_line out "
            else
              failwith "
              *)
          end
  end