sig
  type symbol = Symbol.symbol
  type literal = Term.literal
  type clause = Term.clause
  type arities = (int * Problem.symbol list) list
  class type problem =
    object
      method addClause : Problem.clause -> unit
      method addClauses : Problem.clause list -> unit
      method addToInitialInterpretation : Problem.literal list -> unit
      method containsEquality : bool
      method getClauses : Problem.clause list
      method getConstantSymbols : Problem.symbol list
      method getFunctionArities : Problem.arities
      method getFunctionSymbols : Problem.symbol list
      method getInitialInterpretation : Problem.literal list
      method getMaxClauseLength : int
      method getPredicateArities : Problem.arities
      method getPredicateSymbols : Problem.symbol list
      method isBS : bool
      method isHorn : bool
    end
  val create :
    ?equality:bool ->
    ?horn:bool ->
    Problem.clause list -> Problem.literal list -> Problem.problem
  val update_arities : Problem.arities -> Problem.symbol -> Problem.arities
  val get_arity : Problem.arities -> int -> Problem.symbol list
end