The enumerated set wizard should generate normalized predicates so that the prover is not unnecessarily stressed with tons of predicates to normalize.
This means producing predicates of form "¬x = y" rather than "x ≠ y".
Logged In: YES user_id=1041912 Originator: YES
Done and committed to CVS.
Log in to post a comment.
Logged In: YES
user_id=1041912
Originator: YES
Done and committed to CVS.