Quiero verificar una fórmula del formulario:

Exists p . ForAll x != 0 . f(x, p) > 0

Una implementación (que no funciona) es la siguiente:

def f0(x0, x1, x, y):
    return x1 ** 2 * y + x0 ** 2 * x

s = Solver()
x0, x1 = Reals('x0 x1')
p0, p1 = Reals('p0 p1')

s.add(Exists([p0, p1], 
                ForAll([x0, x1], 
                          f0(x0, x1, p0, p1) > 0
                      )
            ))
#s.add(Or(x0 != 0, x1 != 0))

while s.check() == sat:
    m = s.model()
    m.evaluate(x0, model_completion=True)
    m.evaluate(x1, model_completion=True)
    m.evaluate(p0, model_completion=True)
    m.evaluate(p1, model_completion=True)
    print m
    s.add(Or(x0 != m[x0], x1 != m[x1])) 

La fórmula no está satisfecha.

Conf0() >= 0, la única salida es(0, 0).

Quiero tenerf0() > 0 y restringir(x0, x1) != (0, 0).

Algo que esperaría es:p0, p1 = 1, 1 o2, 2 por ejemplo, pero no sé cómo eliminar0, 0 de los posibles valores parax0, x1.