sig
  type var = Logtk.FOTerm.var
  type term = Logtk.FOTerm.t
  type clause = Logtk.Literals.t
  type form = Cut_form.clause list
  type t = private { vars : Logtk.FOTerm.VarSet.t; cs : Cut_form.form; }
  val make : Logtk.Literals.t list -> Cut_form.t
  val trivial : Cut_form.t
  val equal : t -> t -> bool
  val hash : t -> int
  val compare : t -> t -> int
  val pp : t CCFormat.printer
  val to_string : t -> string
  val pp_tstp : Cut_form.t CCFormat.printer
  val vars : Cut_form.t -> Logtk.FOTerm.VarSet.t
  val cs : Cut_form.t -> Logtk.Literals.t list
  val ind_vars : Cut_form.t -> Cut_form.var list
  val subst1 : Cut_form.var -> Cut_form.term -> Cut_form.t -> Cut_form.t
  val apply_subst :
    renaming:Logtk.Subst.Renaming.t ->
    Logtk.Subst.t -> Cut_form.t Logtk.Scoped.t -> Cut_form.t
  val are_variant : Cut_form.t -> Cut_form.t -> bool
  val normalize : Cut_form.t -> Cut_form.t
  val to_s_form : Cut_form.t -> Logtk.TypedSTerm.Form.t
  module Pos :
    sig
      val at : Cut_form.t -> Logtk.Position.t -> Cut_form.term
      val lit_at :
        Cut_form.t -> Logtk.Position.t -> Logtk.Literal.t * Logtk.Position.t
      val clause_at :
        Cut_form.t -> Logtk.Position.t -> Cut_form.clause * Logtk.Position.t
      val replace :
        Cut_form.t -> at:Logtk.Position.t -> by:Cut_form.term -> Cut_form.t
      val replace_many :
        Cut_form.t -> Cut_form.term Logtk.Position.Map.t -> Cut_form.t
    end
  module Seq :
    sig
      val terms : Cut_form.t -> Cut_form.term Sequence.t
      val terms_with_pos :
        ?subterms:bool ->
        Cut_form.t -> Cut_form.term Logtk.Position.With.t Sequence.t
    end
end