assign(max_seconds, 30).

formulas(sos).

  (x * e) * x = x.
  x * (x * y) = y.
  (x * y) * (z * u) = (x * z) * (y * u).
  ((x * x) * x) * x = e.

end_of_list.

formulas(goals).

  e * e = e.

end_of_list.