  We describe a method and tool called \textit{ContractCheck} that allows for
the consistency analysis of legal contracts, in particular Sales Purchase
Agreements (SPAs). The analysis relies on an encoding of the premises for the
execution of the clauses of an SPA as well as the proposed consistency
constraints using decidable fragments of first-order logic. Textual SPAs are
first encoded in a structured natural language format, called blocks.
\textit{ContractCheck} interprets these blocks and constraints and translates
them in first-oder logic assertions. It then invokes a Satisfiability Modulo
Theories (SMT) solver in order to establish the executability of a considered
contract by either providing a satisfying model, or by providing evidence of
contradictory clauses that impede the execution of the contract. We illustrate
the application of \textit{ContractCheck} and conclude by proposing directions
for future research.
