output tweaks

README.md

@@ -22,10 +22,9 @@ The file [Examples.lean](https://github.com/siddhartha-gadgil/Saturn/blob/main/S
 One can run a compiled version in a command line. This solves the basic examples in the file [Examples.lean](https://github.com/siddhartha-gadgil/Saturn/blob/main/Saturn/Examples.lean) and also the [N-Queens problem](https://en.wikipedia.org/wiki/Eight_queens_puzzle) (if one chooses) for specified `N`. To run this assuming a recent version of the `lean` toolchain is installed using `elan`, one can do the following (in linux) for example:
 
 ```bash
-$ lake build bin
-$ build/bin/saturn 7
+$ lake exe nqueens 7
 ```
 
 The above commands run the basic examples and the 7-queens problem. Without an argument (such as `7` in the above example) just the basic examples are run. 
 
-Note that the performance is slow, to a large extent because the underlying collections used are not optimized for performance.
+Note that the performance is slow, to some extent because the underlying collections used are not optimized for performance.

nqueens.lean

@@ -20,6 +20,7 @@ def printSolution {n dom : Nat}: (clauses : Vector (Clause (n * n)) dom) → Nat
         | .unsat .. =>
           IO.println soln.toString
         | .sat model .. =>
+          IO.println "\nSAT\n"
           IO.println (showQueens  (m + 1) model)
         return ()
 
@@ -34,7 +35,7 @@ def main (args: List String) : IO UInt32 := do
   IO.println ""
   IO.println "SATurn: A SAT solver-prover in lean"
   IO.println ""
-  IO.println "Solving the sat problem with clauses {P ∨ Q}, {P} and {¬Q}:"
+  IO.println "Solving the sat problem with clauses {P ∨ Q}, {¬P} and {¬Q}:"
   IO.println (solveSAT eg1Statement).toString
   IO.println ""
   IO.println "Solving the sat problem with clauses {P ∨ Q} and {¬Q}:"