Converting First order logic to CNF

Is there a existing implementation in C/c++/java to conver开发者_开发百科t first order logic to CNF ?

It might be more efficient to use something like: Boolean Normal Form

For implementation, I recommend doing it yourself for something simple like this. An efficient method has psuedo code + explanation here