Proving First-Order Theorems Using OTTER