let print_multiplication_tables (context: context) (out: out_channel) (problem: problem) (bound: bound) : unit =
  (* print the sorts and domain elements *)
  let domain_size =
    bound#current_bound
  in

  (* find all posible result combinations for a constant/function *)  
  let rec find_result symbol subterms domain_element : int =
    if domain_element > domain_size then begin
      failwith ("print_multiplication_tables: " ^ Symbol.to_string symbol);
    end
            
    else begin
      subterms.(Symbol.arity symbol + 1) <- Finite_domain.get_domain_element domain_element;
      let relation_literal =
        Term.request_literal true
          (Term.request_func (Symbol.get_fd_relation (Symbol.arity symbol + 2), subterms))
      in
        if is_true context relation_literal then
          domain_element
        else
          find_result symbol subterms (domain_element + 1)
    end
  in

  (* build all argument vectors for a function/predicate *)
  let rec enumerate_arguments symbol subterms print position =
    (* done *)
    if position > Symbol.arity symbol then begin
      (* check results *)
      let result =
        find_result symbol subterms 1
      in
        print subterms result
      end
      
    else begin
      (* use each domain element and extend to full argument vector *)
      for i = 1 to domain_size do
        subterms.(position) <- Finite_domain.get_domain_element i;
        enumerate_arguments symbol subterms print (position + 1);
      done;
    end
  in
    
  (* build all argument vectors for a predicate *)
  let rec enumerate_arguments' symbol subterms print position =
    (* done *)
    if position > Symbol.arity symbol then begin
      (* check results *)
      let relation_literal =
        Term.request_literal true
          (Term.request_func (symbol, subterms))
      in
        if is_true context relation_literal then
          print relation_literal
        else
          ()
    end
      
    (* use each domain element and extend to full argument vector *)
    else begin
      for i = 1 to domain_size do
        subterms.(position - 1) <- Finite_domain.get_domain_element i;
        enumerate_arguments' symbol subterms print (position + 1);
      done;
    end
  in

  (* print the multiplication tables *)
  Print.output_line out ("Domain size: " ^ string_of_int domain_size);
  Print.output_line out "";

  (* print the constants *)
  Print.output_line out ("Constants: ");
  List.iter
    (fun symbol ->
      let constant =
        Term.request_const (Symbol.create_fd_symbol symbol)
      in
      let print _subterms result =
        Print.output_line out
          (Term.term_to_string constant ^ " = " ^ Term.term_to_string (Finite_domain.get_domain_element result));
      in
        enumerate_arguments symbol [| constant; constant |] print 1
    )
    (List.sort Symbol.compare_name (List.find_all Symbol.is_input problem#getConstantSymbols));
  Print.output_line out "";
    

  (* print the functions *)
  Print.output_line out ("Functions: ");
  List.iter
    (fun (arity, symbols) ->
      List.iter
        (fun symbol ->
          let symbol_term =
            Term.request_const (Symbol.create_fd_symbol symbol)
          in
          let subterms =
            Array.create (arity + 2) symbol_term
          in
          let print subterms result =
            let subterms' =
              Array.sub subterms 1 (Symbol.arity symbol);
            in
            let function_term =
              Term.request_func (symbol, subterms')
            in
              Print.output_line out
                (Term.term_to_string function_term ^ " = "
                ^ Term.term_to_string (Finite_domain.get_domain_element result));
          in
            enumerate_arguments symbol subterms print 1;
            Print.output_line out "";
        )
        (List.sort Symbol.compare_name (List.find_all Symbol.is_input symbols))
    )
    problem#getFunctionArities;
  Print.output_line out "";

  (* print the predicates *)
  Print.output_line out ("Predicates: ");
  List.iter
    (fun (arity, symbols) ->
      List.iter
        (fun symbol ->
          Print.output_line out (Symbol.to_string symbol ^ ":");
          let subterms =
            Array.create arity (Term.request_var (Var.create_parametric 0))
          in
          let print literal =
            Print.output_line out (Term.term_to_string literal.Term.atom)
          in
            enumerate_arguments' symbol subterms print 1;
            Print.output_line out "";
        )
        (List.sort Symbol.compare_name (List.find_all Symbol.is_input symbols))
    )
    problem#getPredicateArities