В следующем рабочем примере, Как получить соответствующую модель?

     S,   (cl_3,cl_39,cl_11, me_32,m_59,m_81) = 
     EnumSort('S', ['cl_3','cl_39','cl_11','me_32','me_59','me_81'])

       h1, h2 = Consts('h1 h2', S)
       def fun(h1 , h2):

        conds = [
        (cl_3, me_32),
        (cl_39, me_59),
        (cl_11, me_81),
         # ...
             ]

    and_conds = (And(h1==a, h2==b) for a,b in conds)
     return Or(*and_conds)

Например: как следующий solverI '

  s = Solver()
  x1 = Const('x1', S)
  x2 = Const('x2', S)
  s.add(fun(x1,x2)) 

  print s.check()
  print s.model()