% Confluence => UNF
%   from Marc Bezem

true => domain(a), domain(b), domain(c).   %1
e(b,c) => goal .                           %2
true => s(a,b),s(a,c) .                    %3
r(b,Z) => false .                          %4
r(c,Z) => false .                          %5
domain(X) => e(X,X) .                      %6
e(X,Y) => e(Y,X) .                         %7
e(X,Y),e(Y,Z) => e(X,Z) .                  %8
e(X,Y),r(Y,Z) => r(X,Z) .                  %9
e(X,Y) => s(X,Y) .                         %10
r(X,Y) => s(X,Y) .                         %11
s(X,Y),s(Y,Z) => s(X,Z) .                  %12
s(X,Y),s(X,Z) => domain(U),s(Y,U),s(Z,U) . %13
s(X,Y) => e(X,Y);domain(Z),r(X,Z),s(Z,Y) . %14