sig
  type clause = Term.clause
  exception EMPTY_CLAUSE of
              (Preprocessing_resolution.clause *
               Preprocessing_resolution.clause)
  val compute_resolvents :
    print:bool ->
    Preprocessing_resolution.clause list ->
    Preprocessing_resolution.clause list
end