Bug in expressions with quantifiers

[TheAeryan]

I have been trying different FOL expressions with quantifiers and equality (Eq).

Firstly, strict_proves seems to provide incorrect results for many expressions. For example:

# Expression for testing whether predicate P is true for three or more different constants
>>> strict_proves((P(a)), EX(x, EX(y, EX(z, P(x) & P(y) & P(z) & ~Eq(x,y) & ~Eq(y,z) ))))
True
>>> proves((P(a)), EX(x, EX(y, EX(z, P(x) & P(y) & P(z) & ~Eq(x,y) & ~Eq(y,z) ))))
False

Secondly, proves gets stuck when given expressions with many nested quantifiers. For example:

# Function gets stuck and never returns
proves((P(a), P(b)), EX(x,EX(y,EX(z, P(x) & P(y) & P(z) & ~Eq(x,y) & ~Eq(y,z)))))