  We propose a new calculus SCL(EQ) for first-order logic with equality that
only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven
Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal
model assumption is used to guide inferences that are then guaranteed to be
non-redundant. Redundancy is defined with respect to a dynamically changing
ordering derived from the ground literal model assumption. We prove SCL(EQ)
sound and complete and provide examples where our calculus improves on
superposition.
