SATisfying the High School Identities but not Wilkie's Identity

Abstract

We settle an open question related to Tarski's High School Algebra problem by showing that no 11-element algebra can satisfy the High School Identities while refuting Wilkie's identity. We encode the search as a SAT instance and independently verify the result. As a byproduct, we obtain a new 12-element countermodel that is not isomorphic to the previously known one.