8cb140d6cf2c7fa8fce70aa7ba8beb882e66d36fcdc7a61b277755f42095e7a5  mccarthy2.smt2