  This note reports on some experiments, using a handful of standard automated
reasoning tools, for exploring Steinitz-Rademacher polyhedra, which are models
of a certain first-order theory of incidence structures. This theory and its
models, even simple ones, presents significant, geometrically fascinating
challenges for automated reasoning tools.

Logic;Discrete Mathematics;Logic in Computer Science