You can compute a rewriting system by: rewrite = H3.rewriting_system()
Then rewrite.reduce(a1*b1/a1/b1*a2*b2/a2/b2*a3*b3/a3/b3) gives you 1 as expected. But the rewriting system is not confluent by default, and it only has the one rule: a1*b1*a1^-1*b1^-1*a2*b2*a2^-1*b2^-1*a3*b3*a3^-1*b3^-1 ---> 1.