assign(max_seconds, 30). formulas(sos). y * (z * (((u * u') * (x * z)') * y))' = x # label(gt_sax). end_of_list. formulas(goals). (x * y) * z = x * (y * z) # label(associativity). x * x' = y * y' # label(inverse). x * (y * y') = x # label(identity). end_of_list.