Using a theorem prover for reasoning on constraint problems