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").