diff --git a/README.md b/README.md
index 4404c72..c892be0 100644
--- a/README.md
+++ b/README.md
@@ -1,11 +1,11 @@
 [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
 
-Bosphorus is an ANF simplification and solving tool. It takes as input an ANF over GF(2) and can simplify it and also solve it. As a plus, it can also take in a CNF, convert it to ANF, simplify it, then either give a (hopefully simplified) CNF, an ANF, or can run a SAT solver directly and solve it. It uses the following systems: CryptoMiniSat, espresso, M4RI and PolyBoRi (BriAl, a version of PolyBoRi).
+Bosphorus is an ANF simplification and solving tool. It takes as input an ANF over GF(2) and can simplify it and also solve it. As a plus, it can also take in a CNF, convert it to ANF, simplify it, then either give a (simplified) CNF, an ANF, or can run a SAT solver directly and solve it. It uses the following systems: CryptoMiniSat, espresso, M4RI and PolyBoRi (actually BriAl, a version of PolyBoRi).
 
 This work was done by Davin Choo and Kian Ming A. Chai from DSO National Laboratories Singapore, and Mate Soos and Kuldeep Meel from the National University of Singapore (NUS). If you use Bosphorus, please cite our [paper](https://www.comp.nus.edu.sg/~meel/Papers/date-cscm19.pdf) ([bibtex](https://www.comp.nus.edu.sg/~meel/bib/CSCM19.bib)) published at DATE 2019. Some of the code was generously donated by [Security Research Labs, Berlin](https://srlabs.de/).
 
 # Usage
-The main use of the system is to simplify and solve ANF problems. It excels at this and should give you highly optimised CNFs (and correspondigly good solving times) given any ANF. However, it can also simplify and solve CNF problems. When simplifying or solving CNF problems, the CNF is (extremely) naively translated to ANF, then simplifications are applied, and a sophisticated system then translates the ANF back to CNF. This CNF can then be optinally solved.
+The main use of the system is to simplify and solve ANF problems. It excels at this and should give you highly optimised ANFs and also CNFs. Its ANF simplifications should be useful is many areas, not just direct ANF-to-SAT solving. For example, it could well be useful for helping to break [post-quantum cryptograpy problems](https://csrc.nist.gov/projects/post-quantum-cryptography). It can also simplify and solve CNF problems. When simplifying or solving CNF problems, the CNF is (extremely) naively translated to ANF, then simplifications are applied, and a sophisticated system then translates the ANF back to CNF. This CNF can then be optinally solved.
 
 ## Simple Docker usage