Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning