1%
2% ((xy)z)(xz)' = y is a single axiom for Abelian groups in terms
3% of product and inverse.
4%
5
6set(knuth_bendix).
7assign(max_proofs, 4).
8
9clear(print_kept).
10clear(print_new_demod).
11clear(print_back_demod).
12
13assign(stats_level, 1).
14
15list(usable).
16x = x.
17end_of_list.
18
19list(passive).
20f(a,g(a)) != f(b,g(b)) | $Ans(R_inverse).
21f(a,f(b,g(b))) != a | $Ans(R_ident).
22f(f(a,b),c) != f(a,f(b,c)) | $Ans(assoc).
23f(a,b) != f(b,a) | $Ans(commute).
24end_of_list.
25
26list(sos).
27f(f(f(x,y),z),g(f(x,z))) = y.  % 421  (3.2.1)
28end_of_list.
29