assign(max_seconds, 3600).

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

assign(max_weight, 50).

list(weights).
% Penalize deep equations by adding the depth to the symbol count.

weight(x = y) = (weight(x) + weight(y)) + depth(x = y).

end_of_list.

formulas(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.

set(restrict_denials).

formulas(goals).

f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # label(dist_long).
f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_short).
f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) & f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_both).

end_of_list.