BMP is a MACLISP version of the Boyer-Moore theorem prover. It can be run at SAIL by typing .r BMP READ BMP.CLT[UP,DOC] for more information. Gripes etc. → CLT