% The axioms specify a trivial monoid (every string can be reduced to the empty string).
% A convergent set of rules will be produced. However, the number of rules created in the process
% exceeds the value of the Ackermann function A(n,m), where n and m are represented by the number
% of b-s in the last axiom of section (a): ub...bab...bae. Note that m is represented by the
% first chain of b-s, and n by the second. Thus, ubbbabbae represents A(2,3).
% For more details and background information see:
% "On The Problem Of Generating Small Convergent Systems", Journal of Symbolic Computation (1993) 16, 167-187
% by Klaus Madlener, Andrea Sattler-Klein, Friedrich Otto

% axioms

% (a)
wu = Uf
fb = Bf
faae = Fbcd
BF = Fb
UF = r
faab = Sbab
faaa = Sbaa
BS = Sb
US = u
Ufab = uba
Bfab = SabK
Kb = bCK
Ka = aa
Cb = bC
Ca = ab
wo = o
ubbbabbbae = o

% (b)
irbc = O
cX = bc
OX = O

% (c)
iob =
wb =
wa =
Oa =
Oob =
Od =
wS =
UX =
ra =

% ordering & preorder
ordering: syl-r w > i > f > U > B > K > C > X > b > a > e > F > S > d > c > r > u > o > O

% no goals