In [59]: sol(2)
a+b+1
a*b

Out[59]: [a > 0, b > 0, a + b + 1 == a*b]

In [63]: res.check()
Out[63]: sat

In [64]: res.model()
Out[64]: [b = 2, a = 3]


In [65]: res = sol(8)
a*b*c*d*e*f*g+a*b*c*d*e*f*h+a*b*c*d*e*g*h+a*b*c*d*f*g*h+a*b*c*e*f*g*h+a*b*d*e*f*g*h+a*c*d*e*f*g*h+b*c*d*e*f*g*h+1
a*b*c*d*e*f*g*h

In [66]: res.check()