Learning clauses by tracing derivations.