set(auto).
assign(order, kbo).   % Knuth-Bendix ordering
set(lex_order_vars).

terms(weights).
% Penalize deep equations by adding the depth to the symbol count.
% The following means weight(x = y) is weight(x) + weight(y) + depth(x = y).
(x = y) = (x + y) + depth(x = y).
end_of_list.

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).

end_of_list.

clauses(goals).

f(f(A,B,C),D,E) != f(f(A,D,E),f(B,D,E),f(C,D,E)) # answer(dist_long).
% f(f(A,B,C),D,E) != f(A,f(B,D,E),f(C,D,E)) # answer(dist_short).

end_of_list.