unicode_fol_kit.so_find_countermodel

unicode_fol_kit.so_find_countermodel(formula, max_size=3, max_candidates=4194304)

Return a finite structure in which the SO formula FAILS, or None (bounded).

A returned structure witnesses that formula is not second-order valid (free object variables are universally closed, so it refutes the closed reading).

Parameters:

• formula (Node)

• max_size (int)

• max_candidates (int)

Return type:

Structure | None