LADR includes some mathematical programs like: prover 9 (automated theorem prover for first-order and equational logic) mace4 (search for finite models and counterexamples)