sig
  type flag
  type t = private {
    id : int;
    lits : Logtk.Literal.t array;
    trail : Trail.t;
    mutable flags : SClause.flag;
  }
  val make : trail:Trail.t -> Logtk.Literal.t array -> SClause.t
  val equal : SClause.t -> SClause.t -> bool
  val compare : SClause.t -> SClause.t -> int
  val hash : SClause.t -> int
  val id : SClause.t -> int
  val lits : SClause.t -> Logtk.Literal.t array
  val trail : SClause.t -> Trail.t
  val is_empty : SClause.t -> bool
  val length : SClause.t -> int
  val update_trail : (Trail.t -> Trail.t) -> SClause.t -> SClause.t
  val to_s_form :
    ?ctx:Logtk.Term.Conv.ctx -> SClause.t -> Logtk.TypedSTerm.Form.t
  val flag_lemma : SClause.flag
  val flag_persistent : SClause.flag
  val flag_redundant : SClause.flag
  val flag_backward_simplified : SClause.flag
  val set_flag : SClause.flag -> SClause.t -> bool -> unit
  val get_flag : SClause.flag -> SClause.t -> bool
  val new_flag : unit -> SClause.flag
  val mark_redundant : SClause.t -> unit
  val is_redundant : SClause.t -> bool
  val mark_backward_simplified : SClause.t -> unit
  val is_backward_simplified : SClause.t -> bool
  val pp_vars : SClause.t CCFormat.printer
  val pp : SClause.t CCFormat.printer
  val pp_zf : SClause.t CCFormat.printer
  val pp_tstp : SClause.t CCFormat.printer
  val pp_tstp_full : SClause.t CCFormat.printer
  val pp_trail : Trail.t CCFormat.printer
  val pp_trail_tstp : Trail.t CCFormat.printer
  val pp_in : Logtk.Output_format.t -> SClause.t CCFormat.printer
  val proof_tc : SClause.t Logtk.Proof.Result.tc
  val mk_proof_res : SClause.t -> Logtk.Proof.Result.t
  val adapt : Logtk.Proof.S.t -> SClause.t -> Logtk.Proof.S.t
end