% ***************************************************************************
% Sh-2 is a single axiom for Boolean Algebra in terms of the Sheffer stroke.
%
%    f(f(f(y, f(x, y)), y), f(x, f(z, y))) = x # label("Sh-2").
%
% This Prover9 input file derives (in 3 proofs) the following known system.
%
%    f(f(x, x), f(x, x)) = x # label("Sheffer_1").
%    f(x, f(y, f(y, y))) = f(x, x) # label("Sheffer_2").
%    f(f(x, f(y, z)), f(x, f(y, z))) = f(f(f(y, y), x), f(f(z, z), x))
%       # label("Sheffer_3").
%
% Reference:
%
%    Short Single Axioms for Boolean Algebra
%    W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist and L. Wos
%    Journal of Automated Reasoning 29(1):1-16, 2002.
% ***************************************************************************

assign(order,kbo).
set(lex_order_vars).

set(para_from_small).

assign(max_weight,5).

clear(back_demod).
set(restrict_denials).

clear(cac_redundancy).

formulas(assumptions).

   f(f(f(y, f(x, y)), y), f(x, f(z, y))) = x # label("Sh-2").

end_of_list.

formulas(goals).

   f(f(x, x), f(x, x)) = x # label("Sheffer_1").
   f(x, f(y, f(y, y))) = f(x, x) # label("Sheffer_2").
   f(f(x, f(y, z)), f(x, f(y, z))) = f(f(f(y, y), x), f(f(z, z), x))
      # label("Sheffer_3").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

f(f(x,x),f(x,x)) = x.
f(f(f(x,f(y,x)),x),f(y,f(z,x))) = y.
f(f(c1,c1),f(c1,c1)) != c1.
f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),f(u,f(x,f(y,z))))) = f(f(z,f(x,z)),z).
f(f(f(f(x,y),f(f(f(y,f(z,y)),y),f(x,y))),f(x,y)),z) = f(f(y,f(z,y)),y).
f(f(f(x,f(y,x)),x),f(y,f(f(z,f(x,z)),z))) = y.
f(f(f(f(f(x,f(y,x)),x),f(f(f(y,f(z,y)),y),f(f(x,f(y,x)),x))),f(f(x,f(y,x)),x)),z) = f(f(y,f(z,y)),y).
f(x,f(f(f(x,f(x,x)),x),f(y,f(x,f(x,x))))) = f(f(x,f(x,x)),x).
f(x,f(f(f(x,f(x,x)),x),x)) = f(f(x,f(x,x)),x).
f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x)) = x.
f(f(f(f(f(x,f(x,x)),x),f(y,f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)),f(y,x)) = y.
f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),x)) = f(f(x,f(x,x)),x).
f(f(f(f(f(x,f(f(f(x,f(x,x)),x),x)),x),f(x,f(f(f(x,f(x,x)),x),x))),f(f(x,f(f(f(x,f(x,x)),x),x)),x)),f(x,f(f(f(x,f(x,x)),x),x))) = f(f(f(f(x,f(x,x)),x),f(f(x,f(f(f(x,f(x,x)),x),x)),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(f(f(x,f(x,x)),x),x),f(x,f(f(f(x,f(x,x)),x),x))),f(f(x,f(f(f(x,f(x,x)),x),x)),x)),f(x,f(f(f(x,f(x,x)),x),x))) = f(f(f(f(x,f(x,x)),x),f(f(x,f(f(f(x,f(x,x)),x),x)),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(x,f(f(f(x,f(x,x)),x),x)),x)),f(x,f(f(f(x,f(x,x)),x),x))) = f(f(f(f(x,f(x,x)),x),f(f(x,f(f(f(x,f(x,x)),x),x)),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)),f(f(f(x,f(x,x)),x),x)),f(x,f(f(f(x,f(x,x)),x),x))) = f(f(f(f(x,f(x,x)),x),f(f(x,f(f(f(x,f(x,x)),x),x)),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)).
f(f(f(f(x,f(x,x)),x),f(f(x,f(f(f(x,f(x,x)),x),x)),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)) = f(f(f(x,f(x,x)),x),f(x,f(f(f(x,f(x,x)),x),x))).
f(f(f(f(x,f(x,x)),x),f(f(x,f(f(f(x,f(x,x)),x),x)),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)) = x.
f(f(f(f(x,f(x,x)),x),f(f(f(x,f(x,x)),x),f(f(x,f(x,x)),x))),f(f(x,f(x,x)),x)) = x.
f(f(x,f(x,x)),x) = f(x,x).
f(f(x,x),f(f(x,f(x,x)),x)) = x.
$F.
f(x,f(y,f(y,y))) = f(x,x).
f(c2,f(c3,f(c3,c3))) != f(c2,c2).
f(f(x,f(f(y,f(x,y)),y)),f(x,f(z,f(f(y,f(x,y)),y)))) = x.
f(f(f(f(x,f(y,z)),f(u,f(x,f(y,z)))),f(x,f(y,z))),f(u,x)) = u.
f(f(f(f(x,f(y,x)),x),f(f(x,f(f(f(x,f(y,x)),x),x)),x)),y) = f(f(x,f(y,x)),x).
f(f(f(f(x,y),f(z,f(x,y))),f(x,y)),f(z,x)) = z.
f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),f(f(f(z,f(x,z)),z),x)) = f(f(z,f(x,z)),z).
f(f(x,f(x,f(f(y,f(x,y)),y))),f(x,x)) = x.
f(f(f(f(x,x),x),f(x,x)),f(f(x,f(x,f(f(y,f(x,y)),y))),f(z,f(x,x)))) = f(x,f(x,f(f(y,f(x,y)),y))).
f(f(f(f(f(x,x),y),f(f(x,f(x,f(f(z,f(x,z)),z))),f(f(x,x),y))),f(f(x,x),y)),x) = f(x,f(x,f(f(z,f(x,z)),z))).
f(f(f(x,f(y,x)),x),f(y,f(x,f(f(z,f(x,z)),z)))) = y.
f(f(f(f(x,f(f(y,f(x,y)),y)),f(f(f(x,f(z,x)),x),f(x,f(f(y,f(x,y)),y)))),f(x,f(f(y,f(x,y)),y))),z) = f(f(x,f(z,x)),x).
f(f(f(x,f(f(f(f(x,f(y,z)),x),f(x,f(y,z))),x)),x),f(f(z,f(x,z)),z)) = f(f(f(x,f(y,z)),x),f(x,f(y,z))).
f(f(f(f(x,f(f(y,f(x,y)),y)),x),f(x,f(f(y,f(x,y)),y))),x) = f(f(x,f(x,x)),x).
f(f(f(x,f(f(y,f(x,y)),y)),x),f(x,f(f(y,f(x,y)),y))) = f(f(f(x,f(f(x,f(x,x)),x)),x),f(f(y,f(x,y)),y)).
f(f(f(f(x,f(f(x,f(x,x)),x)),x),f(f(y,f(x,y)),y)),x) = f(f(x,f(x,x)),x).
f(f(f(f(x,f(x,x)),x),x),f(f(x,f(x,x)),x)) = x.
f(f(x,x),f(x,f(y,x))) = x.
f(f(f(f(x,f(y,x)),x),f(f(x,f(y,x)),x)),y) = f(f(x,f(y,x)),x).
f(f(f(x,f(y,x)),x),f(y,f(x,f(x,x)))) = y.
f(f(f(x,f(f(f(f(x,f(y,x)),x),f(x,f(y,x))),x)),x),f(x,x)) = f(f(f(x,f(y,x)),x),f(x,f(y,x))).
f(f(f(f(x,f(f(y,f(x,y)),y)),f(f(f(x,f(x,x)),x),f(x,f(f(y,f(x,y)),y)))),f(x,f(f(y,f(x,y)),y))),f(x,f(x,x))) = f(f(x,f(f(x,f(x,x)),x)),x).
f(f(f(x,f(f(y,f(x,y)),y)),x),f(x,f(f(y,f(x,y)),y))) = f(f(f(x,f(x,x)),x),f(f(y,f(x,y)),y)).
f(f(f(f(x,f(x,x)),x),f(f(y,f(x,y)),y)),x) = f(f(x,f(x,x)),x).
f(f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(y,f(x,y)),y))),x) = f(x,f(f(y,f(x,y)),y)).
f(f(f(x,x),x),f(f(x,f(x,x)),x)) = x.
f(f(f(f(x,f(f(y,f(x,y)),y)),x),f(x,f(f(y,f(x,y)),y))),f(x,f(x,x))) = f(f(x,f(f(x,f(x,x)),x)),x).
f(f(f(x,x),x),f(x,x)) = x.
f(x,f(f(x,f(x,f(f(y,f(x,y)),y))),f(z,f(x,x)))) = f(x,f(x,f(f(y,f(x,y)),y))).
f(f(f(x,x),f(f(y,f(x,y)),y)),x) = f(f(x,f(x,x)),x).
f(f(f(x,x),f(f(y,f(x,y)),y)),x) = f(x,x).
f(f(f(x,f(x,x)),x),f(f(f(x,x),f(f(y,f(x,y)),y)),f(x,f(x,x)))) = f(f(x,x),f(f(y,f(x,y)),y)).
f(f(f(x,f(f(y,f(x,y)),y)),x),f(x,f(f(y,f(x,y)),y))) = f(f(x,x),f(f(y,f(x,y)),y)).
f(f(x,x),f(f(f(x,x),f(f(y,f(x,y)),y)),f(x,f(x,x)))) = f(f(x,x),f(f(y,f(x,y)),y)).
f(f(f(x,x),f(f(y,f(x,y)),y)),f(x,f(x,x))) = f(f(x,f(f(x,f(x,x)),x)),x).
f(f(f(x,x),f(f(y,f(x,y)),y)),f(x,f(x,x))) = f(f(x,f(x,x)),x).
f(f(f(x,x),f(f(y,f(x,y)),y)),f(x,f(x,x))) = f(x,x).
f(f(x,x),f(f(y,f(x,y)),y)) = f(f(x,x),f(x,x)).
f(f(x,x),f(f(y,f(x,y)),y)) = x.
f(f(f(x,f(f(y,y),x)),x),y) = f(y,y).
f(f(f(f(f(x,x),f(x,x)),f(f(x,f(x,f(f(y,f(x,y)),y))),f(f(f(z,f(f(f(x,x),f(x,x)),z)),z),f(x,x)))),f(f(x,x),f(x,x))),x) = f(x,f(x,f(f(y,f(x,y)),y))).
f(f(f(f(f(x,f(y,x)),x),f(f(f(x,f(y,x)),x),f(f(x,f(y,x)),x))),f(f(x,f(y,x)),x)),f(f(f(x,f(y,x)),x),f(f(x,f(y,x)),x))) = f(f(y,f(f(f(f(x,f(y,x)),x),f(f(x,f(y,x)),x)),y)),y).
f(f(f(f(x,f(f(y,f(x,y)),y)),f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(y,f(x,y)),y)))),f(x,f(f(y,f(x,y)),y))),f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(y,f(x,y)),y)))) = f(f(x,f(f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(y,f(x,y)),y))),x)),x).
f(f(f(f(x,f(y,x)),x),f(x,f(y,x))),x) = f(x,x).
f(f(f(x,f(y,x)),x),f(x,f(y,x))) = f(f(f(x,f(x,x)),x),f(x,x)).
f(f(f(x,f(y,x)),x),f(x,f(y,x))) = f(f(x,x),f(x,x)).
f(f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(y,f(x,y)),y))),f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(y,f(x,y)),y)))) = f(f(x,f(f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(y,f(x,y)),y))),x)),x).
f(f(f(x,f(y,x)),x),f(x,f(y,x))) = x.
f(f(f(f(x,f(y,x)),x),f(x,f(y,x))),f(f(f(x,f(y,x)),x),x)) = f(f(x,f(y,x)),x).
f(x,f(f(f(x,f(y,x)),x),x)) = f(f(x,f(y,x)),x).
f(f(f(f(x,f(y,x)),x),f(f(f(x,f(y,x)),x),x)),y) = f(f(x,f(y,x)),x).
f(f(f(x,f(f(x,f(x,f(f(y,f(x,y)),y))),f(f(f(z,f(f(f(x,x),f(x,x)),z)),z),f(x,x)))),f(f(x,x),f(x,x))),x) = f(x,f(x,f(f(y,f(x,y)),y))).
f(f(f(x,f(x,f(f(y,f(x,y)),y))),f(f(x,x),f(x,x))),x) = f(x,f(x,f(f(y,f(x,y)),y))).
f(f(f(x,f(x,f(f(y,f(x,y)),y))),x),x) = f(x,f(x,f(f(y,f(x,y)),y))).
f(f(x,f(f(f(x,f(f(y,f(x,y)),y)),f(x,f(f(y,f(x,y)),y))),x)),x) = f(x,f(f(y,f(x,y)),y)).
f(f(x,f(x,f(f(y,f(x,y)),y))),x) = f(x,f(f(y,f(x,y)),y)).
f(f(x,f(f(y,f(x,y)),y)),x) = f(x,f(x,f(f(y,f(x,y)),y))).
f(f(f(f(x,f(y,x)),x),f(f(x,f(y,x)),x)),f(f(f(x,f(y,x)),x),f(f(x,f(y,x)),x))) = f(f(y,f(f(f(f(x,f(y,x)),x),f(f(x,f(y,x)),x)),y)),y).
f(f(x,f(f(f(f(y,f(x,y)),y),f(f(y,f(x,y)),y)),x)),x) = f(f(y,f(x,y)),y).
f(f(x,f(f(y,f(x,y)),y)),x) = f(f(y,f(x,y)),y).
f(x,f(x,f(f(y,f(x,y)),y))) = f(f(y,f(x,y)),y).
f(f(f(x,f(y,x)),x),f(f(f(x,f(y,x)),x),f(f(f(x,f(y,x)),x),f(x,f(y,x))))) = f(f(f(x,f(y,x)),f(f(f(x,f(y,x)),x),f(x,f(y,x)))),f(x,f(y,x))).
f(f(f(x,f(y,x)),f(f(f(x,f(y,x)),x),f(x,f(y,x)))),f(x,f(y,x))) = f(f(f(x,f(y,x)),x),f(f(f(x,f(y,x)),x),x)).
f(f(f(x,f(y,x)),x),f(f(f(x,f(y,x)),x),x)) = f(f(f(x,f(y,x)),x),f(x,f(y,x))).
f(f(f(x,f(y,x)),x),f(f(f(x,f(y,x)),x),x)) = x.
f(f(x,f(y,x)),x) = f(x,y).
f(f(x,y),f(y,f(z,x))) = y.
f(f(x,x),f(y,x)) = x.
f(x,f(y,f(x,x))) = f(x,x).
f(f(x,y),f(y,f(x,z))) = y.
f(f(f(x,y),f(x,z)),z) = f(x,z).
f(f(x,f(y,x)),x) = f(y,x).
f(f(x,y),f(y,y)) = y.
f(f(x,y),f(x,x)) = x.
f(f(x,y),f(x,f(z,y))) = x.
f(f(x,f(y,z)),f(x,y)) = x.
f(x,y) = f(y,x).
f(f(x,f(y,z)),f(z,x)) = x.
f(f(x,y),f(x,f(y,z))) = x.
f(f(x,f(y,z)),f(y,x)) = x.
f(f(x,f(y,z)),f(x,z)) = x.
f(f(x,f(y,f(x,z))),y) = f(y,f(x,z)).
f(x,f(y,f(x,f(y,z)))) = f(x,f(y,z)).
f(f(f(x,f(y,z)),z),x) = f(x,f(y,z)).
f(x,f(f(x,y),f(z,y))) = f(x,y).
f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = f(f(x,f(y,z)),f(y,x)).
f(f(x,f(y,f(x,z))),y) = f(y,f(z,x)).
f(x,f(y,f(x,y))) = f(x,x).
f(f(x,f(y,x)),y) = f(y,y).
f(f(x,f(y,z)),f(f(y,x),x)) = f(f(x,f(y,z)),f(x,f(y,z))).
f(x,f(y,y)) = f(x,f(y,x)).
f(f(x,y),f(f(z,f(y,z)),y)) = y.
f(f(x,y),y) = f(y,f(x,x)).
f(f(x,f(y,z)),f(x,f(u,f(y,x)))) = x.
f(x,f(y,z)) = f(x,f(z,y)).
f(f(x,y),z) = f(z,f(y,x)).
f(x,f(y,f(x,f(z,f(y,x))))) = f(x,x).
f(x,f(y,f(z,f(x,y)))) = f(x,f(y,y)).
f(x,f(y,f(f(y,x),z))) = f(x,f(y,y)).
f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(y,z)),f(x,f(y,y))).
f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,y)) = f(x,f(y,y)).
f(f(x,f(f(y,z),x)),f(y,y)) = f(f(y,z),f(y,y)).
f(f(x,f(f(y,z),x)),f(y,y)) = y.
f(x,f(f(y,f(f(x,z),y)),x)) = f(y,f(f(x,z),y)).
f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(f(x,f(y,f(x,z))),y)).
f(x,f(f(y,f(y,f(z,x))),x)) = f(y,f(y,f(z,x))).
f(x,f(y,f(z,f(z,f(u,f(y,x)))))) = f(x,f(y,y)).
f(x,f(y,f(y,f(z,f(x,y))))) = f(x,f(y,f(x,x))).
f(x,f(y,f(y,f(z,f(x,y))))) = f(x,x).
f(f(f(x,x),y),f(f(z,z),y)) = f(f(y,f(x,z)),f(y,f(x,z))).
f(f(f(c4,c4),c5),f(f(c6,c6),c5)) != f(f(c5,f(c4,c6)),f(c5,f(c4,c6))).
f(f(f(f(x,f(y,x)),x),f(x,f(y,x))),f(f(x,f(y,x)),f(f(x,x),f(x,f(y,x))))) = f(x,f(y,x)).
f(x,f(f(x,f(y,x)),f(f(x,x),f(x,f(y,x))))) = f(x,f(y,x)).
f(x,f(f(x,f(y,x)),x)) = f(x,f(y,x)).
f(x,f(y,x)) = f(x,f(x,y)).
f(f(f(x,y),y),f(y,f(z,x))) = f(f(y,f(z,x)),f(y,f(z,x))).
f(x,f(y,y)) = f(x,f(x,y)).
f(f(x,y),f(z,u)) = f(f(u,z),f(y,x)).
f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,f(f(y,y),f(y,y))).
f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,z))).
f(x,f(f(y,y),f(z,f(x,f(x,y))))) = f(x,y).
f(x,f(f(f(y,f(z,x)),f(y,f(z,x))),f(z,z))) = f(x,f(y,f(z,x))).
f(x,f(y,f(z,z))) = f(x,f(y,f(z,x))).
f(x,f(y,f(f(z,z),x))) = f(x,f(y,z)).
f(f(f(x,x),y),f(z,u)) = f(f(u,z),f(y,f(x,f(u,z)))).
f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,f(f(z,z),x)))).
f(f(x,f(y,z)),f(x,f(y,z))) = f(f(x,f(z,z)),f(x,f(y,f(x,f(z,z))))).

end_of_list.
