clauses(sos).

  y * (z * (((u * u') * (x * z)') * y))' = x.  % GT single axiom

end_of_list.

clauses(sos).

  (A * B) * C != A * (B * C) # answer(associativity).

  A * A' != B * B' # answer(inverse).

  A * (B * B') != A # answer(identity).

end_of_list.