Would you actually use this program for real-world applications of theorem proving, e.g. validating an integrated circuit design before spending millions on its manufacturing?