Bug in expressions with quantifiers

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)))))
```