 Applying automated reasoning strategies again, Ernst, Fitelson, Harris &amp; Wos 2001) discovered several new bases, including the following 2-axiom basis of length 18 and six 1-axiom bases matching Meredith’s length of 21 (only one of these is given below): 