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