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

clauses(sos).

  f(x,x,y) = x                        # label(majority).
  f(f(x,w,y),z,w) = f(w,x,f(w,z,y))   # label(associativity2).

  f(A,B,C) != f(C,A,B) | f(A,B,C) != f(A,C,B) # answer(2a_2b).

end_of_list.