====== Nenofar = Negation Normal Form Automated Reasoner ======

{{{{nenufar.jpg?200|Nenuphar = Water Lily}}

Available downloads:
  * a Linux binary of Nenofar compiled statically against libstdc++ and libc : [[http://lara.epfl.ch/~psuter/nenofar-dist/nenofar]]
  * the compressed sources: [[http://lara.epfl.ch/~psuter/nenofar-dist/nenofar.tgz]]
  * the benchmarks: [[http://lara.epfl.ch/~psuter/nenofar-dist/benchmarks.tgz]]

For more information:
  * [[http://people.epfl.ch/philippe.suter|Philippe Suter]]
  * [[http://infoscience.epfl.ch/record/126445|Non-Clausal Satisfiability Modulo Theories]] (master's thesis by Philippe Suter)