I'm getting this Limit reached: too high cardinality (65536)
error from Isabelle's Nitpick tool:
Nitpicking formula...
[...]
The type 'a passed the monotonicity test; Nitpick might be able to skip some scopes
Using SAT solver "MiniSat" The following solvers are configured: "MiniSat", "SAT4J", "SAT4J_Light", "Lingeling_JNI",
"CryptoMiniSat_JNI", "MiniSat_JNI"
Trying 1 scope:
card 'a = 4
Limit reached: too high cardinality (65536); skipping scope
Nitpick checked 0 of 1 scope
Total time: 63 ms
Questions:
Further information:
The property being checked involves finding filter bases on a topology with four points. This means we're searching for an element (a filter) in a space with $2^4=16$ elements. There are of the order of $65536=2^16=2^{2^4}$ such spaces.
Thank you.
For completeness, the maintainer of nitpick answered and:
I'm afraid your problem is really too big for Nitpick. Not only it hits a technical limit imposed by its backend, Kodkod, problems of this size even if they were accepted by Nitpick would be much too big to be solvable.