sig
  val parsimony_threshold_1 : int Pervasives.ref
  val parsimony_threshold_2 : int Pervasives.ref
  val p_pn_nnf : ?do_pnf:bool -> Formula.formula -> Formula.formula
  val ff_tnf :
    ?force_parsimony:int ->
    (Formula.formula -> Formula.formula -> bool) ->
    Formula.formula -> Formula.formula
  val promote_rels :
    Aux.Strings.t -> Formula.formula -> Formula.formula -> bool
  val ffsep :
    Aux.Strings.t ->
    Aux.Strings.t ->
    Formula.formula ->
    (Formula.fo_var list * Formula.formula list * Formula.formula) list
end