sig
  type t = int -> Logtk.Literal.t -> bool
  val res : Clause_intf.S.clause -> Clause_intf.S.Eligible.t
  val param : Clause_intf.S.clause -> Clause_intf.S.Eligible.t
  val eq : Clause_intf.S.Eligible.t
  val arith : Clause_intf.S.Eligible.t
  val filter : (Logtk.Literal.t -> bool) -> Clause_intf.S.Eligible.t
  val max : Clause_intf.S.clause -> Clause_intf.S.Eligible.t
  val pos : Clause_intf.S.Eligible.t
  val neg : Clause_intf.S.Eligible.t
  val always : Clause_intf.S.Eligible.t
  val combine : Clause_intf.S.Eligible.t list -> Clause_intf.S.Eligible.t
  val ( ** ) :
    Clause_intf.S.Eligible.t ->
    Clause_intf.S.Eligible.t -> Clause_intf.S.Eligible.t
  val ( ++ ) :
    Clause_intf.S.Eligible.t ->
    Clause_intf.S.Eligible.t -> Clause_intf.S.Eligible.t
  val ( ~~ ) : Clause_intf.S.Eligible.t -> Clause_intf.S.Eligible.t
end