assign(max_seconds, 3600).

assign(max_weight, 60).

assign(new_constants, 1).

set(lex_order_vars).

set(restrict_denials).

formulas(sos).

  f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x # label(MOL_SS).

end_of_list.

formulas(goals).

% f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS).
  f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))) # answer(MOD_SS).

end_of_list.