We plan to add educational solvers and tools for
first order predicate logic in the future.
Meanwhile we recommend these options for learning

- Automated Theorem Proving Course Content by Geoff Sutcliffe is probably the best introductory material
- Handbook of Practical Logic and Automated Reasoning contains code examples in ML in addition to an excellent text
- Handbook of Automated_Reasoning for in-depth papers (here on Amazon).

- Otter: a classic, easy-to-use prover by McCune
- The TPTP Problem Library for Automated Theorem Proving by Geoff Sutcliffe and Christian Suttner.
- Online solvers on TPTP
- The CADE ATP System Competition

- SMT (satisfiability modulo theories) solvers used for formal verification like Z3 and PVS
- Answer set based solvers like DLV and Smodels, see the competition
- Description logic solvers, see the list of implementations
- OWL (web ontology language) solvers used in the context of semantic web, see the list of implementations