Mini SMT Solver reasoning about the quality theory. Project for the Automatic Deduction course in MPRI.