DESCR 127 B

123
  1. Prover9, Mace4, and several related programs come packaged in a system
  2. called LADR (Library for Automated Deduction Research).