Business rules control and constrain the behavior and structure of the business system in terms of its policies and principles. Business rules are restructured frequently as per the internal or external circumstances based on market opportunities, statutory regulations, and business focus. Unfortunately, the current practice in industry, of detecting inconsistencies manually, becomes tedious and error prone, due to the size, complexity and ambiguity in representation using natural language. The approach presented in this work to detect inconsistencies in business rules is based on model checking that exploits the FOL basis of SBVR specification. In this paper, we aim to reduce the burden on solvers and obtain effective system level test data, leading to the development of a novel inconsistency rule checker based on extracting the unsatisfiable cores using solvers like Z3, CVC4, etc. We introduce the concept of graphical clusters, to partition SBVR vocabularies and represent the former exploiting the many-sorted logic and graph reachability algorithm, thus reducing the domain of quantification and the number of uninterpreted functions. The translation of SBVR to SMT-LIBv2 is implemented as part of our tool BuRRiTo which employs certain FOL solvers. Experimental results are shown on industrial level rule sets with seeded inconsistencies.