--- xkcd287_Z3.py	2021-02-12 05:12:53.685491965 +0200
+++ xkcd287_Z3_sexpr.py	2021-07-14 02:17:55.920663814 +0300
@@ -6,6 +6,8 @@
 s = Solver()
 s.add(215*a + 275*b + 335*c + 355*d + 420*e + 580*f == 1505, a>=0, b>=0, c>=0, d>=0, e>=0, f>=0)
 
+print(s.sexpr())
+
 results=[]
 
 # enumerate all possible solutions: