sig
  type form = LogtkFormula.FO.t
  type symbol = LogtkSymbol.t
  val is_cnf : LogtkCnf.form -> bool
  val is_lit : LogtkCnf.form -> bool
  val is_clause : LogtkCnf.form list -> bool
  val miniscope : ?distribute_exists:bool -> LogtkCnf.form -> LogtkCnf.form
  type clause = LogtkCnf.form list
  type options =
      DistributeExists
    | DisableRenaming
    | InitialProcessing of (LogtkCnf.form -> LogtkCnf.form)
    | PostNNF of (LogtkCnf.form -> LogtkCnf.form)
    | PostSkolem of (LogtkCnf.form -> LogtkCnf.form)
  val cnf_of :
    ?opts:LogtkCnf.options list ->
    ?ctx:LogtkSkolem.ctx -> LogtkCnf.form -> LogtkCnf.clause list
  val cnf_of_list :
    ?opts:LogtkCnf.options list ->
    ?ctx:LogtkSkolem.ctx -> LogtkCnf.form list -> LogtkCnf.clause list
end