I have a formula in FOL:
$\forall x \exists y: B(x) \implies C(y)$
and in SPASS: forall([X], exists[Y], implies(B(X),C(Y)))
I want to check the formula: $\exists x: B(X) \implies C(X)$ and in SPASS exists([X], implies(B(X), C(X)))
The problem is I want to determine that X and Y are different (like in my first formula) and I want to be the second formula false because of the fact, that B and C are for the same X: $B(X) => C(X)$ but my first formula said that it should be different.
Is there a way to tell SPASS that these arguments should be different?
