On Using First-Order Theorem Provers in a the Jahob Data Structure Verification System