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.