sig
  type symbol = Symbol.symbol
  type term = Term.term
  type clause = Term.clause
  type problem = Problem.problem
  type arities = Problem.arities
  type sorts = Sort_inference.sorts
  type finite_domain
  val create :
    print_transformation:bool ->
    print_sorts:bool -> Finite_domain.problem -> Finite_domain.finite_domain
  val get_problem : Finite_domain.finite_domain -> Finite_domain.problem
  val get_flattened : Finite_domain.finite_domain -> Finite_domain.problem
  val get_sorts : Finite_domain.finite_domain -> Finite_domain.sorts
  val get_axioms :
    print:bool ->
    print_tptp:bool ->
    use_functionality_axioms:bool ->
    Finite_domain.finite_domain -> int -> Finite_domain.clause list
  val get_domain_element : int -> Term.term
  val get_domain_elements : int -> Term.term list
  val relation_to_equations :
    Finite_domain.finite_domain ->
    Finite_domain.term -> Finite_domain.term list
end