Simple clause learning over theories SCL(T) is a decision procedure for the Bernays-Schoenfinkel fragment over bounded difference constraints BS(BD). The BS(BD) fragment consists of clauses built from first-order literals without function symbols together with simple bounds or difference constraints, where for the latter it is required that the variables of the difference constraint are bounded from below and above. The SCL(T) calculus builds model assumptions over a fixed finite set of fresh constants. The model assumptions consist of ground foreground first-order and ground background theory literals. The model assumptions guide inferences on the original clauses with variables. We prove that all clauses generated this way are non-redundant. As a consequence, expensive testing for tautologies and forward subsumption is completely obsolete and termination with respect to a fixed finite set of constants is a consequence. We prove SCL(T) to be sound and refutationally complete for the combination of the the Bernays Schoenfinkel fragment with any compact theory. Refutational completeness is obtained by enlarging the set of considered constants. For the case of BS(BD) we prove an abstract finite model property such that the size of a sufficiently large set of constants can be fixed a priori.