Automated provers for first order logic, based on sequent calculus, tableaux, model elimination or resolution, include 3TAP, ft, Gandalf, LeanTAP, METEOR, Otter, Prover9, SATURATE, SETHEO and Vampire.
Some other interesting systems are ACL2, ALF, EVES, FOL/GETFOL, IMPS, KIV, Lambda Prolog, LARCH, Metamath, MIZAR, MuRal, NQTHM, OBJ3, OSHL, PVS and TPS.
There are some online collections of problems for theorem provers, notably the TPTP Problem Library. Recent competitions include the CADE13 Competition, the CADE14 Competition, the Beweiserhappening 95 and the Beweiserhappening 97.
Some HOL-specific pages:
I'm intending to compile a description and categorization of automated reasoning systems. But this is still in its early stages.