Otter is a theorem-proving program