let get_axioms ~(print: bool) ~(print_tptp: bool) ~(use_functionality_axioms: bool)
    (finite_domain: finite_domain) (domain_size: int) : clause list =
  if print then begin
    print_newline ();
    print_endline ("Finite domain axioms for domain size " ^ string_of_int domain_size ^ ":");
    print_newline ();
  end;

  (* to ensure evaluation and print order, create axioms in order *)
  let domain_size_axioms =
    get_domain_size_axioms ~print:print ~print_tptp:print_tptp domain_size
  and totality_axioms =
    get_totality_axioms ~print:print ~print_tptp:print_tptp finite_domain domain_size
  and canonicity_axioms =
    if Const.fd_use_canonicity then
      get_canonicity_axioms ~print:print ~print_tptp:print_tptp 
        (Sort_inference.constants_partition finite_domain.sorts) domain_size
    else
      []
  and functionality_axioms =
    if use_functionality_axioms then
      get_functionality_axioms ~print:print ~print_tptp:print_tptp finite_domain domain_size
    else
      []
  and equality_axioms =
    if
      finite_domain.original#containsEquality
      ||
      not finite_domain.term_definitions.definitions#is_empty
    then
      get_equality_axioms ~print:print ~print_tptp:print_tptp domain_size
    else
      []        
  in

  let axioms =
    List.map to_diff_clause
      (domain_size_axioms @ totality_axioms @ canonicity_axioms @ functionality_axioms @ equality_axioms)
  in

  axioms