% The stream of objects to be rewritten can include
% terms, clauses, and formulas.  They are parsed
% as Prover9/LADR "terms".

(a' * b) * (a' * b)'.

y * (z * (((w * w') * (x * z)') * y))' = x.