******************************************
Clauses Relevant to the BA/Sheffer Problem
******************************************

Notation:

   Shi and Ci refer to our JAR paper.

   Ai refers to the 25 candidates from the BA Web page.

   Waldi refers to the two single axioms later found with Waldmeister.

   Suffix _m refers to the mirror image of an equation.

 
Sh1 and Sh2 are the two single axioms presented in our JAR paper.
 
   f(f(x, f(f(y, x), x)), f(y, f(z, x))) = y # label("Sh1/A10").
   f(f(f(y, f(x, y)), y), f(x, f(z, y))) = x # label("Sh2/A14_m").
 
C1..C16 are the other (i.e., not including Sh1 and Sh2) 16 candidates
from our JAR paper.
 
   f(f(y, f(y, f(y, x))), f(x, f(y, z))) = x # label("C1/A1").
   f(f(y, f(y, f(x, y))), f(x, f(z, y))) = x # label("C2/A4/Wald1").
   f(f(y, f(y, f(x, x))), f(x, f(z, y))) = x # label("C3/A6").
   f(f(y, f(y, f(x, z))), f(x, f(z, y))) = x # label("C4/A7").
   f(f(y, f(y, f(z, x))), f(x, f(y, z))) = x # label("C5/A8/Wald2)").
   f(f(y, f(f(x, y), y)), f(x, f(y, z))) = x # label("C6/A9").
   f(f(y, f(y, f(y, x))), f(x, f(z, y))) = x # label("C7/A2").
   f(f(f(f(y, x), y), y), f(x, f(z, y))) = x # label("C8/A12_m").
   f(f(f(f(y, x), z), z), f(x, f(y, z))) = x # label("C9/A13_m"). 
   f(f(f(y, f(y, x)), y), f(x, f(z, y))) = x # label("C10/A16_m").
   f(f(f(y, f(x, x)), y), f(x, f(z, y))) = x # label("C11/A18_m").
   f(f(f(f(y, x), z), z), f(x, f(z, y))) = x # label("C12/A19_m").
   f(f(f(f(y, x), y), y), f(x, f(y, z))) = x # label("C13/A20_m").
   f(f(f(y, f(x, z)), y), f(x, f(y, z))) = x # label("C14/A21_m").
   f(f(f(y, f(z, x)), y), f(x, f(y, z))) = x # label("C15/A23_m").
   f(f(f(y, f(y, x)), y), f(x, f(y, z))) = x # label("C16/A24_m").
 
A1..A25 are the 25 candidates (Equations 1..25) from the BA Web page.

   f(f(x, f(x, f(x, y))), f(y, f(x, z))) = y # label("A1/C1").
   f(f(x, f(x, f(x, y))), f(y, f(z, x))) = y # label("A2/C7").
   f(f(x, f(x, f(y, x))), f(y, f(x, z))) = y # label("A3").
   f(f(x, f(x, f(y, x))), f(y, f(z, x))) = y # label("A4/C2/Wald1").
   f(f(x, f(x, f(y, y))), f(y, f(x, z))) = y # label("A5").
   f(f(x, f(x, f(y, y))), f(y, f(z, x))) = y # label("A6/C3").
   f(f(x, f(x, f(y, z))), f(y, f(z, x))) = y # label("A7/C4").
   f(f(x, f(x, f(y, z))), f(z, f(x, y))) = z # label("A8/C5/Wald2").
   f(f(x, f(f(y, x), x)), f(y, f(x, z))) = y # label("A9/C6").
   f(f(x, f(f(y, x), x)), f(y, f(z, x))) = y # label("A10/Sh1)").
   f(f(x, f(f(y, z), x)), f(y, f(z, x))) = y # label("A11").
   f(f(f(x, y), z), f(x, f(x, f(z, x)))) = z # label("A12/C8_m").
   f(f(f(x, y), z), f(x, f(x, f(z, y)))) = z # label("A13/C9_m").
   f(f(f(x, y), z), f(x, f(f(x, z), x))) = z # label("A14/Sh2_m)").
   f(f(f(x, y), z), f(x, f(f(y, z), x))) = z # label("A15").
   f(f(f(x, y), z), f(x, f(f(z, x), x))) = z # label("A16/C10_m").
   f(f(f(x, y), z), f(x, f(f(z, y), x))) = z # label("A17").
   f(f(f(x, y), z), f(x, f(f(z, z), x))) = z # label("A18/C11_m").
   f(f(f(x, y), z), f(y, f(y, f(z, x)))) = z # label("A19/C12_m").
   f(f(f(x, y), z), f(y, f(y, f(z, y)))) = z # label("A20/C13_m").
   f(f(f(x, y), z), f(y, f(f(x, z), y))) = z # label("A21/C14_m").
   f(f(f(x, y), z), f(y, f(f(y, z), y))) = z # label("A22").
   f(f(f(x, y), z), f(y, f(f(z, x), y))) = z # label("A23/C15_m").
   f(f(f(x, y), z), f(y, f(f(z, y), y))) = z # label("A24/C16_m").
   f(f(f(x, y), z), f(y, f(f(z, z), y))) = z # label("A25").