sig
  val abstract_learn :
    ((string * Formula.formula) list -> Structure.structure option) ->
    Formula.formula -> Formula.formula option
  val find_lfp_iter :
    int ->
    Formula.formula ->
    Formula.formula ->
    Formula.formula option ->
    Formula.formula option -> Formula.formula option
  val basic_outline :
    ?free_id:int ->
    ?neg:bool ->
    ?eq:bool ->
    ?only_pos:bool ->
    ?prefix:string ->
    k:int ->
    c:int ->
    asyms:Formula.formula list Pervasives.ref ->
    (string * int) list ->
    (string * int) list -> string list -> Formula.formula
  val lfp_outline :
    ?free_id:int ->
    ?recursive:bool ->
    ?positive:bool ->
    ?eq:bool ->
    fp:string list ->
    k:int ->
    c:int ->
    asyms:Formula.formula list Pervasives.ref ->
    (string * int) list ->
    (string * int) list ->
    string list -> (int * int * int * int) list -> Formula.formula
end