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.

x * (x \ y) = y.
x \ (x * y) = y.
(x / y) * y = x.
(x * y) / y = x.

end_of_list.

formulas(goals).

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

end_of_list.