sig
  type result
  val initial_result :
    Cfg.cfg ->
    Predicate.predicate_table ->
    Term.symbol_table -> NegativeUnits.store -> Tableau.result
  val first_result :
    Cfg.cfg ->
    Predicate.predicate_table ->
    Term.symbol_table ->
    NegativeUnits.store -> IcSet.clauses -> Tableau.result
  val next_result : Tableau.result -> Tableau.result
  val abandon_result : Tableau.result -> Tableau.result
  val is_open : Tableau.result -> bool
  val info_msg : Tableau.result -> unit
  type refutation
  val get_refutation : Tableau.result -> Tableau.refutation
  val refutation_to_term :
    Term.symbol_table -> Tableau.refutation -> Term.term
  val get_l_proof : Tableau.result -> Fact.l_proof
  val print_compiled_rules :
    Cfg.cfg ->
    Predicate.predicate_table ->
    Term.symbol_table -> NegativeUnits.store -> IcSet.clauses -> unit
end