please review wip/prover9

Please review wip/prover9.  From the DESCR file:

This package includes Prover9, an automated theorem prover
for first-order and equational logic, and Mace4, which
searches for finite models and counter examples.

Thanks,
Pouya

------------------------------------------------------------------------------
Gaining the trust of online customers is vital for the success of any company
that requires sensitive data to be transmitted over the Web.   Learn how to 
best implement a security strategy that keeps consumers' information secure 
and instills the confidence they need to proceed with transactions.
http://p.sf.net/sfu/oracle-sfdevnl