diff --git a/examples/python/socrates.py b/examples/python/socrates.py
index 79a1b57f1..49067225f 100644
--- a/examples/python/socrates.py
+++ b/examples/python/socrates.py
@@ -1,9 +1,9 @@
 ############################################
 # Copyright (c) Microsoft Corporation. All Rights Reserved.
-# 
-# all humans are mortal
-# Socrates is a human
-# so Socrates mortal 
+#
+# all humans are mortal
+# Socrates is a human
+# so Socrates mortal 
 ############################################
 
 from z3 import *
@@ -15,10 +15,10 @@ Object = DeclareSort('Object')
 Human = Function('Human', Object, BoolSort())
 Mortal = Function('Mortal', Object, BoolSort())
 
-# a well known philosopher 
+# a well known philosopher 
 socrates = Const('socrates', Object)
 
-# free variables used in forall must be declared Const in python
+# free variables used in forall must be declared Const in python
 x = Const('x', Object)
 
 axioms = [ForAll([x], Implies(Human(x), Mortal(x))), 
@@ -27,7 +27,9 @@ axioms = [ForAll([x], Implies(Human(x), Mortal(x))),
 
 s = Solver()
 s.add(axioms)
-# classical refutation
+# classical refutation
 s.add(Mortal(socrates) == False)
 
-print(s.check()) # prints unsat so socrates is Mortal
+print(s.check()) # prints unsat so socrates is Mortal
+
+# print(s.proof()) # prints a low level (not readable) proof object.