sig
  module E : Env.S
  module Solver : Sat_solver.S
  module BLit = BBox.Lit
  val split : E.multi_simpl_rule
  val check_empty : E.unary_inf_rule
  val before_check_sat : unit Signal.t
  val after_check_sat : unit Signal.t
  val filter_absurd_trails : (Trail.t -> bool) -> unit
  val check_satisfiability : E.generate_rule
  type cut_res = private {
    cut_src : Literals.t list;
    cut_pos : E.C.t list;
    cut_neg : E.C.t list;
    cut_lit : BLit.t;
  }
  val pp_cut_res : Avatar_intf.S.cut_res CCFormat.printer
  val cut_res_clauses : Avatar_intf.S.cut_res -> E.C.t Sequence.t
  val print_lemmas : unit CCFormat.printer
  val introduce_cut : Literals.t list -> ProofStep.t -> Avatar_intf.S.cut_res
  val on_input_lemma : Avatar_intf.S.cut_res Signal.t
  val convert_lemma : E.clause_conversion_rule
  val register : unit -> unit
end