let get_axioms ~(print_axioms: bool) (problem: Problem.problem) : clause list =
  let predicate_symbols, function_symbols =
    problem#getPredicateSymbols, problem#getFunctionSymbols
  in

  let axioms =
    get_equality_clauses ()
  and predicate_substitutions =
    get_predicate_substitutions predicate_symbols
  and function_substitutions =
    get_function_substitutions function_symbols
  in

    if print_axioms then begin
      print_endline ("Equality Axioms:");
      List.iter (fun clause -> print_endline (Term.clause_to_string clause)) axioms;
      print_newline ();
      
      if List.length predicate_substitutions > 0 then begin
        print_endline ("Predicate Substitution Axioms:");
        List.iter (fun clause -> print_endline (Term.clause_to_string clause)) predicate_substitutions;
        print_newline ();
      end;

      if List.length function_substitutions > 0 then begin
        print_endline ("Function Substitution Axioms:");
        List.iter (fun clause -> print_endline (Term.clause_to_string clause)) function_substitutions;
        print_newline ();
      end;
      print_newline ();
    end;

    axioms @ predicate_substitutions @ function_substitutions