% Saved by Prover9-Mace4 Version 0.5, December 2007.

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
  assign(max_megs, 2000).
  assign(max_seconds, 1800).
  assign(max_weight, 300).
  assign(sos_limit, 200).
end_if.

if(Mace4).   % Options for Mace4
  assign(domain_size, 13).
  assign(start_size, 13).
  assign(end_size, 13).
  assign(max_seconds, -1).
  assign(max_megs, 2000).
end_if.

formulas(assumptions).

%with 2,4,no
%size 13: 1497s
%size 12: 27.77s
%size 11: 1.38s

x=y*(x*((y*x)*y)) #label(677).
x=(y*x)*((y*(y*x))*y) #label(consequence677).
((x*y)*z)*x=((x*z)*(y*z))*x #label(16018451).
x*y = x*z -> y = z.
%all x all y exists z (x*z = y).
%exists x -(exists y (y*x = x)).
%exists a (a*a = a).

end_of_list.

formulas(goals).

x=((x*x)*x)*x #label(255).

end_of_list.