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

clauses(sos).

  f(x,x,y) = x                       # label(majority).
  f(x,y,z) = f(z,x,y)                # label(2a).
% f(x,y,z) = f(x,z,y)                # label(2b)
  f(f(x,w,y),w,z) = f(x,w,f(y,w,z))  # label(associativity).

% f(A,B,C) != f(C,A,B)               # answer(2a).
  f(A,B,C) != f(A,C,B)               # answer(2b).

end_of_list.
