% op(400, xfx, f).

set(hyper_res).
set(para_from).
set(para_into).
set(order_eq).
set(input_sos_first).

assign(equiv_hint_wt, 0).
set(keep_hint_subsumers).

assign(max_weight,0).

clear(print_kept).
clear(print_back_sub).
clear(print_new_demod).
clear(print_back_demod).

  
list(usable).

x = x.

% Denial of the Shefferbasis.

f(f(a, a), f(a, a)) != a
	| f(a, f(b, f(b, b))) != f(a, a)
	| f(f(f(b, b), a), f(f(c, c), a)) != f(f(a, f(b, c)), f(a, f(b, c)))
	| $ANS("Sheffer").

end_of_list.

list(passive).

end_of_list.

list(sos).

f(f(x, f(f(y, x), x)), f(y, f(z, x))) = y.  % Sh_1

end_of_list.

% This list of hints guides Otter directly to a particular proof.

list(hints).
f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z)))))=f(z,f(f(x,z),z)).
f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z)=f(y,f(f(z,y),y)).
f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z))))=y.
f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x)))))=f(x,f(f(x,x),x)).
f(x,f(f(x,x),x))=f(x,x).
f(f(x,f(f(x,x),x)),f(x,x))=x.
f(f(x,x),f(x,f(y,x)))=x.
f(f(x,f(f(f(y,y),x),x)),y)=f(y,y).
f(f(f(x,y),f(f(f(x,y),f(x,y)),f(x,y))),f(f(x,y),f(x,y)))=f(y,f(f(f(f(x,y),f(x,y)),y),y)).
f(x,f(f(f(f(y,x),f(y,x)),x),x))=f(y,x).
f(f(x,x),f(y,x))=x.
f(x,f(y,f(x,x)))=f(x,x).
f(f(f(x,y),f(x,y)),y)=f(x,y).
f(x,f(f(y,x),x))=f(y,x).
f(f(x,y),f(x,f(z,y)))=x.
f(f(x,f(y,z)),f(x,z))=x.
f(x,f(f(x,y),f(z,y)))=f(x,y).
f(f(f(x,f(y,z)),z),x)=f(x,f(y,z)).
f(x,f(f(y,x),x))=f(x,y).
f(x,y)=f(y,x).
f(f(x,y),f(x,x))=x.
f(f(x,y),f(y,f(z,x)))=y.
f(f(x,f(y,z)),f(z,x))=x.
f(f(x,y),f(y,f(x,z)))=y.
f(f(x,f(y,z)),f(y,x))=x.
f(f(f(x,y),f(x,z)),z)=f(x,z).
f(x,f(y,f(x,f(y,z))))=f(x,f(y,z)).
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(x,z)).
f(f(x,f(y,z)),f(x,f(u,f(y,x))))=x.
f(f(x,f(y,f(x,z))),y)=f(y,f(z,x)).
f(x,f(y,f(x,f(z,f(y,x)))))=f(x,x).
f(x,f(y,f(x,y)))=f(x,x).
f(x,f(y,z))=f(x,f(z,y)).
f(x,f(y,f(z,f(x,y))))=f(x,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(f(x,f(y,x)),y)=f(y,y).
f(f(x,y),z)=f(z,f(y,x)).
f(x,f(y,x))=f(x,f(y,y)).
f(f(f(x,y),y),f(y,f(z,x)))=f(f(y,f(z,x)),f(y,f(z,x))).
f(f(x,y),f(z,u))=f(f(u,z),f(y,x)).
f(x,f(y,f(f(y,x),z)))=f(x,f(y,y)).
f(f(x,y),y)=f(y,f(x,x)).
f(x,f(y,y))=f(x,f(x,y)).
f(f(x,f(y,y)),f(x,f(z,y)))=f(f(x,f(z,y)),f(x,f(z,y))).
f(f(x,f(y,z)),f(x,f(y,y)))=f(f(x,f(y,z)),f(x,f(y,z))).
f(x,f(f(y,y),f(z,f(x,f(x,y)))))=f(x,f(f(y,y),f(y,y))).
f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,y))=f(x,f(y,y)).
f(x,f(f(y,y),f(z,f(x,f(x,y)))))=f(x,y).
f(f(f(f(x,y),f(x,y)),f(f(z,f(f(x,y),z)),f(x,y))),f(x,x))=f(f(z,f(f(x,y),z)),f(x,x)).
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(x,f(y,f(y,y)))=f(x,x).
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(x,f(y,y)),f(x,f(z,f(f(y,y),x))))=f(f(x,f(z,y)),f(x,f(z,y))).
f(f(x,f(y,y)),f(x,f(z,f(x,f(y,y)))))=f(f(x,f(z,y)),f(x,f(z,y))).
f(f(x,f(y,y)),f(x,f(z,z)))=f(f(x,f(z,y)),f(x,f(z,y))).
f(f(f(x,x),y),f(f(z,z),y))=f(f(y,f(x,z)),f(y,f(x,z))).
end_of_list.