sig
  type term = Term.term
  type literal = Term.literal
  type clause = Term.clause
  type subst = Subst.subst
  type pureness
  val get_pureness : Term_attributes.term -> Term_attributes.pureness
  val is_universal : Term_attributes.pureness -> bool
  val is_mixed : Term_attributes.pureness -> bool
  val is_parametric : Term_attributes.pureness -> bool
  val is_term_parametric : Term_attributes.term -> bool
  val is_propositional : Term_attributes.literal -> bool
  val cmp_pureness :
    Term_attributes.pureness -> Term_attributes.pureness -> int
  val cmp_universality :
    Term_attributes.pureness -> Term_attributes.pureness -> int
  val depth_of_literal : Term_attributes.literal -> int
  val depth_of_term : Term_attributes.term -> int
  val depth_of_literal_subst :
    Term_attributes.literal -> Term_attributes.subst -> int -> int
  val weight_of_literal : Term_attributes.literal -> int
  val weight_of_literal_subst :
    Term_attributes.literal -> Term_attributes.subst -> int -> int
  val weight_of_clause : Term_attributes.clause -> int
end