# Candidate Axiom Systems

The candidate set consists of 25 single equations and 2 pairs of equations, all in terms of the Sheffer stroke operator |.

```  % candidate single axioms
((x | (x | (x | y))) | (y | (x | z))) = y   (Equation 1)
((x | (x | (x | y))) | (y | (z | x))) = y   (Equation 2)
((x | (x | (y | x))) | (y | (x | z))) = y   (Equation 3)
((x | (x | (y | x))) | (y | (z | x))) = y   (Equation 4)
((x | (x | (y | y))) | (y | (x | z))) = y   (Equation 5)
((x | (x | (y | y))) | (y | (z | x))) = y   (Equation 6)
((x | (x | (y | z))) | (y | (z | x))) = y   (Equation 7)
((x | (x | (y | z))) | (z | (x | y))) = z   (Equation 8)
((x | ((y | x) | x)) | (y | (x | z))) = y   (Equation 9)
((x | ((y | x) | x)) | (y | (z | x))) = y   (Equation 10)
((x | ((y | z) | x)) | (y | (z | x))) = y   (Equation 11)
(((x | y) | z) | (x | (x | (z | x)))) = z   (Equation 12)
(((x | y) | z) | (x | (x | (z | y)))) = z   (Equation 13)
(((x | y) | z) | (x | ((x | z) | x))) = z   (Equation 14)
(((x | y) | z) | (x | ((y | z) | x))) = z   (Equation 15)
(((x | y) | z) | (x | ((z | x) | x))) = z   (Equation 16)
(((x | y) | z) | (x | ((z | y) | x))) = z   (Equation 17)
(((x | y) | z) | (x | ((z | z) | x))) = z   (Equation 18)
(((x | y) | z) | (y | (y | (z | x)))) = z   (Equation 19)
(((x | y) | z) | (y | (y | (z | y)))) = z   (Equation 20)
(((x | y) | z) | (y | ((x | z) | y))) = z   (Equation 21)
(((x | y) | z) | (y | ((y | z) | y))) = z   (Equation 22)
(((x | y) | z) | (y | ((z | x) | y))) = z   (Equation 23)
(((x | y) | z) | (y | ((z | y) | y))) = z   (Equation 24)
(((x | y) | z) | (y | ((z | z) | y))) = z   (Equation 25)

% candidate pair
((x | y) | (x | (y | z))) = x   (Equation 26a)
(x | y) = (y | x)   (Equation 26b, Commutativity)

% candidate pair
((x | z) | (x | (y | z))) = x   (Equation 27a)
(x | y) = (y | x)   (Equation 27b, Commutativity)
```

Here is the candidate set in clause form, suitable as input to Otter. f(x,y) denotes x | y, an application of the Sheffer stroke operator.

```  % candidate single axioms
f(f(x, f(x, f(x, y))), f(y, f(x, z))) = y # label("Equation 1").
f(f(x, f(x, f(x, y))), f(y, f(z, x))) = y # label("Equation 2").
f(f(x, f(x, f(y, x))), f(y, f(x, z))) = y # label("Equation 3").
f(f(x, f(x, f(y, x))), f(y, f(z, x))) = y # label("Equation 4").
f(f(x, f(x, f(y, y))), f(y, f(x, z))) = y # label("Equation 5").
f(f(x, f(x, f(y, y))), f(y, f(z, x))) = y # label("Equation 6").
f(f(x, f(x, f(y, z))), f(y, f(z, x))) = y # label("Equation 7").
f(f(x, f(x, f(y, z))), f(z, f(x, y))) = z # label("Equation 8").
f(f(x, f(f(y, x), x)), f(y, f(x, z))) = y # label("Equation 9").
f(f(x, f(f(y, x), x)), f(y, f(z, x))) = y # label("Equation 10").
f(f(x, f(f(y, z), x)), f(y, f(z, x))) = y # label("Equation 11").
f(f(f(x, y), z), f(x, f(x, f(z, x)))) = z # label("Equation 12").
f(f(f(x, y), z), f(x, f(x, f(z, y)))) = z # label("Equation 13").
f(f(f(x, y), z), f(x, f(f(x, z), x))) = z # label("Equation 14").
f(f(f(x, y), z), f(x, f(f(y, z), x))) = z # label("Equation 15").
f(f(f(x, y), z), f(x, f(f(z, x), x))) = z # label("Equation 16").
f(f(f(x, y), z), f(x, f(f(z, y), x))) = z # label("Equation 17").
f(f(f(x, y), z), f(x, f(f(z, z), x))) = z # label("Equation 18").
f(f(f(x, y), z), f(y, f(y, f(z, x)))) = z # label("Equation 19").
f(f(f(x, y), z), f(y, f(y, f(z, y)))) = z # label("Equation 20").
f(f(f(x, y), z), f(y, f(f(x, z), y))) = z # label("Equation 21").
f(f(f(x, y), z), f(y, f(f(y, z), y))) = z # label("Equation 22").
f(f(f(x, y), z), f(y, f(f(z, x), y))) = z # label("Equation 23").
f(f(f(x, y), z), f(y, f(f(z, y), y))) = z # label("Equation 24").
f(f(f(x, y), z), f(y, f(f(z, z), y))) = z # label("Equation 25").

% candidate pair
f(f(x, y), f(x, f(y, z))) = x # label("Equation 26a").
f(x, y) = f(y, x) # label("Equation 26b, Commutativity").

% candidate pair
f(f(x, z), f(x, f(y, z))) = x # label("Equation 27a").
f(x, y) = f(y, x) # label("Equation 27b, Commutativity").
```